I think of forcing in the following context: Truth and Definability Lemmas. So forcing is a schema in the meta theory.
Now in his Set Theory book (the first edition), Kunen claims that setting up the following schema also deals with the mathematics required for showing $ZFC\vdash{\forall{\text{ctm } M \text{ of } {\ulcorner{ZFC}\urcorner}}} \implies \exists{N} (M\subseteq{N} \wedge N \text{ is a ctm of } \ulcorner{ZFC+\neg{CH}}\urcorner)$
Here in order to eliminate the use of relativization we can replace the occurrences of $(\text{Forces}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})})^{M}$ by $M\models\ulcorner\text{Forces}_{\varphi}^{*}\urcorner{[(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})]}$ if we want. That I'm fine with. But I'm not sure how to we can replace the forcing schema with a single theorem inside of $ZFC$ (I would need to do this to verify $N\models{\ulcorner{ZFC}\urcorner}$).
The "follow my nose solution" is to say that after formalizing logic and model theory inside of set theory I can prove (as pointed out by justus87 I don't need to keep the corner notation anymore since I'm proving a result about sets inside of set theory.):
$ZFC\vdash\forall\varphi(x_{1},...,x_{n})\in{Fm_{L=\{\in\}}}$ with all free variables shown, $\exists\text{Forces}_{\varphi}^{*}(x_{1},...,x_{n},y_{1},...,y_{4})\in{Fm_{L=\{\in\}}}$ s.t. $\forall$ ctm $M\models{{ZF-P}}$, $\forall{\mathbb{(P,\leq,1)}}\in{M}$, $\varkappa_{1},...,\varkappa_{n}\in{M^{\mathbb{P}}}, \forall{G}$ that is $\mathbb{P}-$generic over $M$,
a) If $p\in{G}$ and $M\models\text{Forces}^{*}_{\varphi}{(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})}$ then $M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$
b) If $M[G]\models\varphi{({\varkappa_{1}}_{G},...,{\varkappa_{n}}_{G})}$, then there is $p\in{G}$ s.t. $M\models\mbox{Forces}^{*}_{\varphi}(\mathbb{P},\leq,1,p,\varkappa_{1},,...,\varkappa_{n})$
This looks correct and should follow but I'm not a $100\%$ certain. Writing a schema inside the meta-theory as a theorem is somewhat tricky and I haven't quite mastered it (if we try to do this with the reflection theorems and do it improperly we end up obtaining that $ZFC$ is inconsistent).
Edit 1: I realized that I had the symbols for the codes down wrong. Now in this case the codes will be the codes for $L(M)$ and $L(M[G])$
Edit 2: I removed the use of codes after I formalized logic and model theory in ZFC. My initial idea was I would have the original codes for set theoretic formulas and when considering formulas of $L(M)=L\cup{\{c_{m}:m\in{M}\}}$ I could extend the codes in such a way so that the new codes($\ulcorner\urcorner_{1}$) had the property that if $\ulcorner\phi\urcorner_{1}$ used symbols only in $L$, then $\ulcorner\phi\urcorner_{1}=\ulcorner\phi\urcorner$. (It should work even without that, i.e. even if $L(M)$ has new codes that does not extend the old codes we can still insist that the new code $\ulcorner\phi\urcorner_{1}$ represents the formula that was originally represented by $\ulcorner\phi\urcorner$)