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 

 - <cite authors="Habič, Miha E.; Hamkins, Joel David; Klausner, Lukas Daniel; Verner, Jonathan; Williams, Kameryn J.">_Habič, Miha E.; Hamkins, Joel David; Klausner, Lukas Daniel; Verner, Jonathan; Williams, Kameryn J._, [**Set-theoretic blockchains**](https://doi.org/10.1007/s00153-019-00672-z), Arch. Math. Logic 58, No. 7-8, 965-997 (2019). [ZBL1468.03063](https://zbmath.org/?q=an:1468.03063).</cite>

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.