This phenomenon occurs whenever there is a transitive model of ZFC.
Suppose that $M$ is a countable transitive model of ZFC. Let $\newcommand\P{\mathbb{P}}\P$ be the Easton-support class product forcing, adding a Cohen subset to every regular cardinal. Let $M[G]$ be a corresponding forcing extension.
For each amenable class $I\subseteq\text{Ord}^{M}$, meaning that $\langle M,{\in},I\rangle$ is a model of ZFC in the language with predicate $I$, let us consider the restriction $\P\upharpoonright I$, which restricts the forcing to the cardinals of $I$. There is a corresponding model $M[G\upharpoonright I]$, which is a transitive model of $M[G]$. We can view $M[G\upharpoonright I]$ as a forcing extension of the GBC model in which $I$ is available as a predicate, but then we restrict back down to the first-order ZFC model that results.
There are continuum many different amenable classes, since we can force to add a generic class of ordinals, and these are all amenable, and the corresponding models $M[G\upharpoonright I]$ are distinct. Since there is a splitting tree whose branches are generic for this class forcing, there are continuum many such classes.
Most of them will not be definable in $M[G]$, simply because there are too many.
But actually, if $I$ is chosen as mutually generic with $G$ in the manner I've described, then $I$ will not be definable in $M[G]$, since it is generic over $M[G]$, and so $M[G\upharpoonright I]$ will be nondefinable but amenable to $M[G]$.
So we've found a closed set of inner models $M[G\upharpoonright I]$ of $M[G]$, none of which are definable from parameters. But all of them will be amenable to $M[G]$ and so $M[G]$ will satisfy $\text{ZFC}_{M[G\upharpoonright I]}$, making this a dual example to your final request.
But if one wants $M[G]$ to violate $\text{ZFC}_I$, then this can be arranged. One should let $I$ be generic over $M$, but non-amalgamable with $G$. This is possible using the non-amalgamation methods of
- Habič, Miha E.; Hamkins, Joel David; Klausner, Lukas Daniel; Verner, Jonathan; Williams, Kameryn J., Set-theoretic blockchains, Arch. Math. Logic 58, No. 7-8, 965-997 (2019). ZBL1468.03063.
The result is $M[G\upharpoonright I]\subseteq M[G]$, where these are countable transitive ZFC models, with the first not definable in the second and $\text{ZFC}_{M[G\upharpoonright I]}$ fails in $M[G]$.
Finally, let me mention that none of these arguments require well-foundedness. Everything works fine if one simply uses any countable model of ZFC, whether it is well-founded or not. So the phenomenon occurs whenever ZFC is consistent.