I've seen various statements that the Boolean-valued models of ZFC occurring in model-theoretic forcing are "really" the topos of sheaves on an appropriate site, but never a fully precise statement. What *exactly* is the relationship, and where can I find this written down in a clear, simple way?

More precisely, let $\mathbb{P}$ be a poset and $B$ its completion to a Boolean algebra. Then, the machinery of forcing gives a Boolean-valued model of ZFC (let's ignore issues related to the universe, countable transitive models, etc. unless they really become crucial) $V^{(B)}$ such that the truth values of the axioms of ZFC are $1$, and the forcing relation can be defined as $p \Vdash \phi$ for $p \in B$ iff the truth value of $\phi$ is at least $p$.

On the other hand, we may consider $\mathbb{P}$ as a site with the double negation topology (for some $p \in \mathbb{P}$, a collection $S$ of elements $s \in \mathbb{P}$, $s \leq p$ covers $p$ iff for all $q \leq p$ there is some $s \in S$ with $s \leq q$; i.e. $S$ is "dense" below $p$) and take the Boolean topos $\mathscr{V}_\mathbb{P}$ of sheaves on this site. The subsheaves of the terminal object in this topos form a Boolean algebra $\Omega$, and we can assign elements of $\Omega$ as "truth values" of sentences $\phi$ via the Kripke-Joyal semantics. This lets us define a "forcing relation" for $p \in \Omega$ as $p \Vdash' \phi$ iff the terminal map from the Yoneda image of $p$ factors through the truth value of $\phi$.

What is the exact relationship between $V^{(B)}$ and $\mathscr{V}_\mathbb{P}$? In what sense is $\mathscr{V}_\mathbb{P}$ a model of ZFC? (i.e. can it be used directly to prove consistency results in the same way that $V^{(B)}$ can?) I would like to say something like "$p \Vdash \phi$ iff $p \Vdash' \phi$", but strictly speaking this doesn't quite make sense since the formulas are expressed in two slightly different languages (i.e. the language for Kripke-Joyal semantics is that of type theory).

I would love to see this written down in detail somewhere.

(As far as I can tell, a generic filter is not strictly relevant to this question; however, I would be curious if it has an interesting interpretation on the sheaf side).