Let $M$ be a countable model of set theory, and let $\mathbb{M}$ be the generic multiverse on $M$. $\mathbb{M}$ forms a Kripke model for modal logic with $\Diamond \phi$ being true at a world if $\phi$ holds in a forcing extension of that world. The logic in this model is known to be at least $S4.2$.
For $\phi$ in the first order language of set theory, let $\phi^\Diamond$ denote the formula that results by prepending each universal quantifier with a $\Box$ and each existential with a $\Diamond$.
Let $\Phi$ be an arbitrary instance of the replacement schema in the first order language of set theory. Does $\Phi^\Diamond$ hold in $\mathbb{M}$, considered as a Kripke model?
I have an argument that it does, but I'm not sure it's right. Here's a sketch:
Let $W$ be a world of $\mathbb{M}$ and suppose $\forall x \in a \Diamond \exists y \phi^\Diamond(x, y)$. We must show that there is a forcing extension of $W$ that contains a $b$ with $\Box \forall x \in a \Diamond \exists y \in b \phi^\Diamond(x, y)$. Since we can't add elements to sets by forcing, this reduces to showing that there is a $b$ in an extension of $W$ with $\forall x \in a \exists y \in b \Box \Diamond \phi^\Diamond(x, y)$. Since in $S4.2$, any formula of the form $\phi^\Diamond$ is provably equivalent to $\Box \phi^\Diamond$ and $\Diamond \phi^\Diamond$, this in turn reduces to showing $\forall x \in a \exists y \in b \phi^\Diamond(x, y)$. (See e.g. Linnebo, "Thin Objects", Lemma 3.1.)
By assumption, for each $x$ we have an extension $W[G_x]$ with $W[G_x] \models \phi^\Diamond(x, y)$, and by the just cited lemma we also have $W[G_x] \models \Box \phi^\Diamond(x,y)$, so any forcing extension of $W[G_x]$ will similarly satisfy $\phi^\Diamond(x,y)$. Since $M$ is countable we can enumerate the $G_x$s as $\langle G_n : n \in \omega \rangle$. Identify $G_n$ with the product forcing $G_1 \times .... \times G_n$. Since we are dealing only with $x$ in some fixed $a$ in $W$, the cardinality of these forcings $G_n$ is bounded in $W$, and hence (by Fuchs Hamkins & Reitz, 'set theoretic geology', Theorem 39) there is an extension $W[H]$ of all the $W[G_n]$s. This $W[H]$ satisfies $\forall x \in a \exists y \phi^\Diamond(x, y)$, so in $W[H]$ we have $\exists b \forall x \in a \exists y \in b \phi^\Diamond(x, y)$, as req'd.
I'm not super confident in this reasoning, or that the result holds. Any direction is much appreciated.
I'm not sure about the argument you give, but here's how I'd be tempted to go about proving it.
First, we establish a translation between the modalised and unmodalised languages of set theory (where $[x]$ is the cannonical name of $x$ (I forget the actual notation)).
Then we can prove:
$\forall \vec{x}\in w(w\vDash \phi^\Diamond \leftrightarrow w\vDash \phi^*)$
Now, assume that in $w$ for all $y\in x$, $w\vDash \Diamond\exists z\phi^\Diamond(z, y)$. By the lemma, that means for all $y\in x$, there is some $P_y$ and $p_y\in P_y$ and name $z_y$ in $w$ such that $w\vDash p_y\Vdash \phi^*(z_y, [y])$. So, applying Replacement in $w$, we can assume they form a set. Now, $\langle p_y,..., p_{y'},...\rangle$ will be a condition in $P_y\times...\times P_{y'}...$. Let $G_y\times...\times G_{y'}...$ be a generic for this partial order containing that condition. Then it will be the case that:
$w[G_y]\vDash \phi^*(z_y^{G_y}, y)$
and so:
$w[G_y]\vDash \phi^\Diamond(z_y^{G_y}, y)$
And since $w[G]$ is a forcing extension of $w[G_y]$ (by the product forcing lemma) and we have S4.2:
$w[G]\vDash \phi^\Diamond(z_y^{G}, y)$
Finally, the set $t$ of names $z_y...$ etc in $w$ will be in $w[G]$ and thus so will $t^{G}$. So:
$w[G]\vDash \forall y\in x \exists z\in t^{G}\phi^\Diamond(z, y)$
So:
$w\vDash \Diamond\exists t \Box\forall y\in x\Diamond\exists z\in t \phi^\Diamond(z, y)$