For $n\in\omega+1$ let $\mathsf{ZFC}_n$ be $\mathsf{ZC}$ + $\{\Sigma_k$–$\mathsf{Rep}: k<n\}$. Let $\widehat{\mathsf{ZFC}}$ be the strongest consistent theory $\mathsf{ZFC}_n$ (so if $\mathsf{ZFC}$ is consistent then $\widehat{\mathsf{ZFC}}=\mathsf{ZFC}$). Note that this definition is entirely "internal" – for example, for every standard natural number $n$ every model of $\mathsf{ZFC}$ thinks that $\widehat{\mathsf{ZFC}}$ has a model and that $\widehat{\mathsf{ZFC}}$ strictly extends $\mathsf{ZFC}_n$ (see here).
I'm interested in the "downward-looking" modal logic this gives rise to. Ignoring set/class issues for simplicity, let our class of worlds $\mathbb{W}$ be the class of models of $\mathsf{ZFC}$, with the accessibility relation $\mathcal{M}\rightarrow\mathcal{N}$ holding whenever $\mathcal{N}$ is a structure in $\mathcal{M}$ such that $\mathcal{M}\models(\mathcal{N}\models\widehat{\mathsf{ZFC}})$. Intuitively $\Diamond \varphi$ expresses that $\varphi$ is "as consistent as possible" with $\mathsf{ZFC}$.
Finally, and as with for example the modal logic of forcing (see Hamkins), we'll restrict attention to "first-order expressible" valuations $\nu$; these are valuations such that for each propositional atom $p$ there is some sentence in first-order set theory $\varphi$ with $\nu(p)=\{\mathcal{M}\in\mathbb{W}: \mathcal{M}\models\varphi\}.$ Basically, we're not just treating $(\mathbb{W},\rightarrow)$ as a pure Kripke frame, we're also restricting attention to "model-theoretically meaningful" ways of assigning truth values to sentences at worlds.
Question 1: What is the corresponding modal logic? That is, what propositional modal sentences are made true at every world with respect to every valuation satisfying the above expressibility criterion?
Since this is rather broad, let me localize things a bit. Note that we can make sense of the definition of the modal logic above – call it "$\mathfrak{D}$" – within the language of set theory itself, so we can ask what a given model of $\mathsf{ZFC}$ thinks about $\mathfrak{D}$. Semantically, this amounts to restricting attention to worlds within a given model of $\mathsf{ZFC}$.
Question 2: Is there a (standard) propositional modal sentence $\varphi$ such that it is independent of $\mathsf{ZFC}$ whether $\varphi\in\mathfrak{D}$?
A positive answer to question 2 would suggest that question 1 does not have a simple answer.
My primary interest is actually in more complicated languages based on the above picture – in particular, when $\mathcal{M}\rightarrow\mathcal{N}$, the starting structure $\mathcal{M}$ thinks that some of the elements of $\mathcal{N}$ are standard and so we get a partial counterpart relation and can start playing with object quantifiers – but the "pure sentential" side of things seems like a good starting point already.
Best Answer
First point is that this logic is simply the provability logic of formalized $\widehat{\mathsf{ZFC}}$-provability, i.e. the provability logic of the provability predicate: $$\mathsf{Prv}_{\widehat{\mathsf{ZFC}}}(x)\colon\;\;\;\;\; \exists y(\mathsf{Con}(\mathsf{ZFC}_y)\land \mathsf{Prv}_{\mathsf{ZFC}_y}(x)).$$ This, of course. simply is a variant of Feferman's provability (see [1]) for the case of $\mathsf{ZFC}$. The fact that this provability logic coincides with the one based on the frame of models from the question, could be shown in the fashion of the paper [2] of Paula Henk, whom considered the case of $\mathsf{PA}$ with usual provability and the frame built from $\mathsf{PA}$ models. Basically we simply show by induction on the modal depth of modal formulas $\varphi(\vec{x})$ that for any first-order valuation $[\vec{\psi}/\vec{x}]$ and model $\mathcal{M}\models \mathsf{ZFC}$ we have $$\mathcal{M}\Vdash \varphi(\vec{x})[\vec{\psi}/\vec{x}]\iff \mathcal{M}\models (\varphi(\vec{x})[\vec{\psi}/\vec{x}])^{\star},$$ where $\cdot^\star$ is the provability interpretation mapping $\Box$ to $\mathsf{Prv}_{\widehat{\mathsf{ZFC}}}$.
Hence the question is basically what is the provability logic of this version of Feferman provability. The provability logic of Feferman provability for $\mathsf{PA}$ was studied by Vladimir Shavrukov [3]. Namely his main focus was on the provability predicate $$\exists y (\mathsf{Con}(\mathsf{I}\Sigma_{y})\land \mathsf{Prv}_{\mathsf{I}\Sigma_y}(x))$$ Although, I haven't carefully checked this, I am almost sure, that the result would transfer to $\mathsf{Prv}_{\widehat{\mathsf{ZFC}}}$ without any troubles. For the step of induction we simply use that each $\mathcal{M}\models \mathsf{ZFC}$ satisfies completeness theorem.
So assuming that Shavrukov's result indeed transfers, then the joint provability logic of $\mathsf{Prv}_{\mathsf{ZFC}}$ ($\Box$) and $\mathsf{Prv}_{\widehat{\mathsf{ZFC}}}$ ($\triangle$) is
The answer to the original Question 1 is the $\triangle$-fragment of this logic.
[1] S. Feferman. Arithmetization of metamathematics in a general setting. Fundamenta mathematicae, vol. 49 no. 1 (1960), pp. 35–92.
[2] Henk, Paula. "Kripke models built from models of arithmetic." Logic, Language, and Computation: 10th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2013, Gudauri, Georgia, September 23-27, 2013. Revised Selected Papers. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015. https://eprints.illc.uva.nl/id/eprint/489/1/PP-2014-01.text.pdf
[3] Shavrukov, V. Yu. "A smart child of Peano's." Notre Dame Journal of Formal Logic 35.2 (1994): 161-185. https://projecteuclid.org/journalArticle/Download?urlId=10.1305%2Fndjfl%2F1094061859