In Kunen's Set Theory book, forcing is described as a finitistic procedure to get some relative consistency result $Con(ZFC)\Rightarrow Con(T)$, where $T$ is an extension of $ZFC$. Because we can't prove (from $ZFC$) the existence of a countable transitive set model of $ZFC$, Kunen describes the relative consistency proof using a countable set model $M$ of a finite fragment of $ZFC$ with enough strength to carry out the particular argument. Treating this $M$ as the ground model, we can use forcing to attain some $N\supset M$ that models $T$. From here, if we could derive a contradiction $T\vdash\phi\wedge\neg\phi$, then $ZFC$ would derive this contradiction relativized to $N$, i.e. $ZFC\vdash\phi^N\wedge\neg\phi^N$. Since we assume $Con(ZFC)$ in our relative consistency argument, this is a contradiction, so it cannot be the case that $T$ can prove any contradiction and we can conclude $Con(T)$. Kunen remarks that this proof is finitistic as we don't use any infinitistic methods in the metatheory to produce this argument.
I follow the argument, but I was unclear whether it is necessary that the ground model only models a finite fragment of $ZFC$. I know that the incompleteness theorems show that $ZFC$ can't prove the existence of a set model of the entirety of $ZFC$, but can't we assume the existence of one as a consequence of our $Con(ZFC)$ assumption in the relative consistency argument? Earlier in Kunen's book, he mentions that we can use Gödel numbering to define the satisfaction relation with set models and formally prove the completeness theorem as a theorem of $ZFC$. If we assume $Con(ZFC)$ in our proof, it seems like we can use this formal version of the completeness theorem to get the existence of a set model of all of $ZFC$, which we can then treat as the ground model for the forcing argument. I know that deciphering the Gödel numbering requires a metatheorem, but the statements $Con(ZFC)$ and $Con(T)$ are already expressed using Gödel numbering in Kunen's original argument, so invoking the Gödel numbered completeness theorem wouldn't seem to make this argument any less formal or finitistic. Am I misunderstanding something, or is my suggestion just another valid approach to the foundations of forcing?
Another example of this same question comes up when using class models to prove relative consistency results. Kunen provides a similar finitistic argument that the class $L$ can be used to prove $Con(ZF)\Rightarrow Con(ZFC)$, without appealing to the assumed existence of set models of $ZF$ or $ZFC$. In this case could we use the formalized completeness theorem to get a set model $M$ of $ZF$ from the assumption $Con(ZF)$, then use the defining formula for the class $L$ and separation to get a set model for $ZFC$ as a subset of $M$?
Con(ZF) gives you a model, but not necessarily a well-founded model.
(Incidentally, well-foundedness is the real issue, not transitivity. Given a well-founded model, we can always use Mostowski collapse to obtain a transitive model.)
Cohen, in his initial publications, used Axiom SM, "There exists a standard model of ZF". (Standard models are all well-founded, of course.) It is known that Con(ZF) does not imply SM. The reason basically is that the minimal model doesn't satisfy SM, but if Con(ZF) is true, then it satisfies Con(ZF). That's because Con(ZF) is a $\Pi_1$ sentence.
It is possible to carry through the forcing argument with a non-well-founded model, as the linked answer from spaceisdarkgreen remarks. So Con(ZF) would be sufficient.
Incidentally, Cohen eventually did look at non-well-founded models, in a paper on the independence of AC ("Automorphisms of Set Theory", Proceedings of the Tarski Symposium, 1971, pp.325-330). As he remarks in his book, there can be no true automorphism of a standard transitive model of ZF. Forcing proofs thus work with automorphisms of the notion of forcing. But Cohen constructed a true automorphism of a non-well-founded model of ZF and used that to prove the relative consistency of Con(ZF+$\neg$AC).