Formal proof of Con(ZFC) => Con(ZFC + not CH) in ZFC
The reflection principle is a theorem scheme; each of its instances is provable in ZFC.
The following proof works entirely in ZFC:
Assume Con(ZFC) together with not-Con(ZFC+non-CH) and aim for a contradiction.
By assumption plus completeness theorem, there is a model (M,E) of ZFC. M may be nonstandard in the sense that its ordinals (even its natural numbers) are not well-founded.
By compactness, there is some finite sub theory ZFC* of ZFC such that ZFC*+non-CH is inconsistent.
Find a (slightly larger) finite sub theory ZFC** of ZFC such that ZFC** proves all theorems you need about forcing, including that ZFC* plus non-CH holds in the extension.
(M,E) satisfies reflection for ZFC** , so there is some x in M which M thinks is a ctm (countable transitive model) of ZFC** . So M can find a Cohen extension y of x which satisfies ZFC* plus non-CH.
By the easy direction of the completeness theorem, M therefore thinks that ZFC*+non-CH is consistent.
But then this theory is really consistent. (Because any proof of an inconsistency would be coded by a natural number, which is represented in M.)
Btw, I think the sketch I just gave is not ideal since it seems to rely on the existence of infinite sets. The implication from Con(ZFC) to Con(ZFC+non-CH) can really be shown in ZF minus infinity, or even in a weak version of Peano arithmetic.
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.
A careful consideration of the method shows that in fact the relative consistency result Con(ZFC)$\to$Con(ZFC+$\neg$CH) can be made in PA. One need only verify that PA can prove that ZFC proves the required development. But I prefer to leave this to the expertise of the proof theorists.
You have almost answered your own question; it seems that the only part you are confused about is whether "the reflection principle operates outside ZFC."
One must, as always, distinguish between the formal system whose properties we are analyzing (in this case, ZFC), and the theory inside which we are making our arguments about said formal system. The latter is what we call the "meta-theory." When you ask if Con(ZFC)→Con(ZFC+¬CH) can be proved purely within ZFC, this can only mean: "Can the meta-theoretic argument itself be formalized in ZFC?" Note here that ZFC is playing two roles; it is the theory being studied, and also the (meta-)theory being used to prove things about ZFC. It's important to not to confuse these two roles.
Now, the reflection principle takes place "outside ZFC" only in the sense that it is being used in the meta-theoretic proof of Con(ZFC)→Con(ZFC+¬CH). But this doesn't mean that the meta-theoretical argument can't itself be formalized in ZFC; in fact, it can, and in fact it can be formalized in much weaker systems (I think primitive recursive arithmetic suffices).
For more explanation about how to prove Con(ZFC)→Con(ZFC+¬CH) finitistically, I'd recommend Chapter VII, §9 of Kunen's book Set Theory: An Introduction to Independence Proofs. Here is one relevant paragraph:
We show that, given any finite list, $\phi_1, \ldots, \phi_n$, of axioms of, say, ZFC+¬CH, we can prove in ZFC that there is a countable transitive model for $\phi_1, \ldots, \phi_n$. The procedure involves finding (in the metatheory) another finite list $\psi_1, \ldots, \psi_m$ of axioms of ZFC, and proving in ZFC that given a countable transitive model $M$ for $\psi_1, \ldots, \psi_m$, there is a generic extension, $M[G]$, satisfying $\phi_1, \ldots, \phi_n$. The inelegant part of this argument is that the procedure for finding $\psi_1, \ldots, \psi_m$, although straightforward, completely effective, and finitistically valid, is also very tedious. We must list in $\psi_1, \ldots, \psi_m$ not only the axioms of ZFC "obviously" used in checking that $\phi_1, \ldots, \phi_n$ hold in $M[G]$ (e.g., if $\phi_1$ is the Power Set Axiom, then $\phi_1$ should be listed among $\psi_1, \ldots, \psi_m$), but also all the axioms needed to verify that various concepts are absolute for $M$ ("finite", "p.o.", etc.), as well as the axioms needed to show that certain mathematical results, such as the Δ-system lemma, hold in $M$.