What are some examples of a pair $M\subseteq N$ of transitive set models of $\mathsf{ZFC}$ with the same ordinals, such that $M$ is not a definable class (with parameters) in $N$? Is it possible that $N$ doesn't even satisfy $\mathsf{ZFC}_U$, where the unary predicate $U$ is interpreted as $M$ and we have replacement for formulas in the extended language?
I require them to be set models because I'm not sure how to correctly formulate it for classes.
Here is an example from a transitive set model of ZFC + "there is a proper class of measurable cardinals". If there is one, then there is a countable one $N$, so fix such an $N$. Fix a sequence $\left<\kappa_n,U_n\right>_{n<\omega}$ of successor measurables $\kappa_n$ of $N$ cofinal in $\mathrm{OR}^N$, with $\kappa_n<\kappa_{n+1}$, and $U_n\in N$ such that $N\models$"$U_n$ is a $\kappa_n$-complete nonprincipal ultrafilter over $\kappa_n$". Let $M$ be the model given by the length $\omega+1$ iteration of $N$, using the (images of the) $U_n$'s. That is, let $M_0=N$ and $E_0=U_0$ and $M_1=\mathrm{Ult}(M_0,E_0)$ and $i_{01}:M_0\to M_1$ the ultrapower map. Given $M_n$ and $i_{0n}:M_0\to M_n$, let $E_{n+1}=i_{0n}(U_n)$ and $M_{n+1}=\mathrm{Ult}(M_n,E_n)$ and $i_{0,n+1}:M_0\to M_{n+1}$ be $j\circ i_{0n}$ where $j:M_n\to M_{n+1}$ is the ultrapower map. Let $M_\omega$ be the direct limit of the $M_n$. Then $M_\omega$ is a transitive model of ZFC, $M_\omega\subseteq N$, but $M_\omega$ is not definable over $N$. In fact, $(N,M_\omega)$ does not model ZFC$_U$, where $U$ is an added predicate interpreted by $M_\omega$. (Is that what you were asking for in the second part?). For the $\kappa_n$'s are exactly those ordinals $\kappa$ which are measurable in $N$ but not measurable in $M_\omega$.
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
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.
