It seems like we should be able to prove that the existence of a transitive model for ZFC is strictly stronger than Con(ZFC), but I can't find anything saying so / giving an argument for it. Is there a standard way of demonstrating this?
An example of what I'm looking for, if it existed: given Con(ZFC), is there a way of generating a model which models Con(ZFC) but which believes that no models of ZFC are transitive?
Any model of ZFC+Con(ZFC)+$\neg$Con(ZFC+Con(ZFC)) should do. (This theory is, by the second incompleteness theorem, consistent if ZFC+Con(ZFC) is).
Because the model believes Con(ZFC) and also believes that no model of ZFC can believe Con(ZFC), the only models of ZFC it can know will be ones that it considers to have non-standard integers. Non-standard models of arithmetic are never well-founded, so such an internal model cannot be transitive.