The use of the Boolean-valued model approach to forcing allows one to avoid any consideration of countable transitive models in the proof that Con(ZFC) implies Con(ZFC+$\neg$CH), and gives in my opinion a more satisfying account of the result by dealing directly with models of full ZFC, rather than working with models only of some fragment of set theory. The point is that we have a very general procedure enabling us, starting from any model of ZFC, to produce a closely related model of ZFC+$\neg$CH.
Specifically, suppose that $M$ is any model of ZFC. By the standard development of Boolean-valued models, as for example explained in Timothy Chow's A beginner's guide to forcing, or my notes on An introduction to the Boolean ultrapower, one may inside $M$ define the $\mathbb{B}$-valued model $M^{\mathbb{B}}$, where $\mathbb{B}$ is the Boolean algebra in $M$ of the forcing $\text{Add}(\omega,\omega_2)^M$. These developments of forcing show that every axiom of ZFC gets Boolean value $1$ in $M^{\mathbb{B}}$, and further that $\|\neg\text{CH}\|=1$. Let $U$ be any ultrafilter on $\mathbb{B}$ in $M$, and form the quotient $M^{\mathbb{B}}/U$. The Los theorem for Boolean ultrapowers shows that this is a first-order structure satisfying every statement whose Boolean value is in $U$. In particular, $M^{\mathbb{B}}/U$ satisfies ZFC+$\neg$CH.
So we've shown that if there is a model of ZFC, then there is a model of ZFC+$\neg$CH, and this establishes the relative consistency result, as desired.
The key to the success of the method is to develop the method of forcing internally in ZFC via the $\mathbb{B}$-valued universe and its quotient. Thus, the construction of the model $M^{\mathbb{B}}$ and the quotient $M^{\mathbb{B}}/U$ is undertaken entirely inside the model $M$, as an internal ZFC construction. By this means, forcing becomes sensible over any model of ZFC.
By formalizing the details
A careful consideration of how this argument proceeds, one may in the end prove method shows that in fact the relative consistency result Con(ZFC)$\to$Con(ZFC+$\neg$CH) can be made in PA, but . One need only verify that PA can prove that ZFC proves the required development. But I will let prefer to leave this to the expertise of the proof theoristsexplain this.

