What are some further examples of proper class models of ZF that are contained in their own "self-relativization"? Let $\Gamma$ and $\Delta$ be theories in the language of set theory (LST), and let $M = \{x: \phi(x)\}$ be a class, where $\phi(x)$ is some formula of LST.  Let us say that $M$ is a (standard) class model of $\Gamma$ in $\Delta$ if and only if $\Gamma \vdash \psi$ implies $\Delta \vdash \psi^M$ for all sentences $\psi$ of LST, where $\psi^M$ denotes the relativization of $\psi$ to the class $M$.  I'm curious about what can be said of proper class models $M$ of ZF in ZF such that $\mbox{ZF} \vdash \forall x (x \in M \rightarrow \phi^M(x)$), i.e., $\mbox{ZF} \vdash \forall x (\phi(x) \rightarrow \phi^M(x))$.
A class $M = \{x: \phi(x)\}$ satisfying $\forall x (\phi(x) \rightarrow \phi^M(x))$ could be said to be "contained in its self-relativization."  Using Definition I.16.5 from Kunen's set theory book (2013), the statement $\forall x (\phi(x) \rightarrow \phi^M(x))$ (i.e., $(\forall x \, \phi(x))^\phi)$) holds if and only if $\phi$ is absolute for $\{x:\phi(x)\}$, written $\{x: \phi(x)\} \preceq_\phi V$.
Examples of such proper class models of ZF satisfying this self-relativization property are $V$ and $L$ (and both satisfy the stronger condition $\mbox{ZF} \vdash \forall x (\phi(x) \leftrightarrow \phi^M(x)$).  Note also that the canonical inner models $L[0^\sharp]$, $L[\mu]$, etc., are transitive class models of ZF that satisfy the self-relativization property, but their consistency strength is well beyond that of ZF.
My questions are as follows.  What are some other interesting examples and non-examples?  Am I correct in thinking that HOD is a non-example? Are there examples besides $V$ and $L$ whose existence is equiconsistent with ZF?  And is there an example that is non-transitive?
One interesting thing about such class models $M$ of ZF in ZF is that ZF does not refute $V = M$ if ZF is consistent, for if $\mbox{ZF} \vdash \neg \forall x (\phi(x))$, then $\mbox{ZF} \vdash \neg \forall x (x\in M \rightarrow \phi^M(x))$, and therefore $\mbox{ZF} \nvdash \forall x (x \in M \rightarrow \phi^M(x))$, assuming ZF is consistent.  This is what piqued my interest in the question. Also, one of the comments points out that, if ZF proves that $M$ is non-transitive, then ZF refutes $V = M$.  Thus, if there is a non-transitive example, then ZF cannot prove that it is non-transitive.  But could there be one that isn't transitive according to a theory stronger than ZF?  (Maybe no such theory would be very natural or attractive.)
 A: Let $AC$ stand for the axiom of choice, let $L$ denote the constructible universe and let $L^*$ the universe of constructible sets transitively containing $\emptyset$ as an element.
Although $L^*$ is a proper subclass of $L$, it collapses to $L$, so it is isomorphic to $L$.
Let $\phi(x)$ be the formula

*

*$(AC\rightarrow x\in L)\wedge(\neg AC\rightarrow x\in L^*)$.

I claim that the corresponding class $M$ is a model of $ZFC$ in $ZF$. In fact, $M$ is either $L$ or  $L^*$, so it is a model of $ZFC$ in any case.
(This argument can be made precise: $ZF\vdash AC\rightarrow (\psi^M\leftrightarrow \psi^L)$ and $ZF\vdash \neg AC\rightarrow (\psi^M\leftrightarrow \psi^{L^*})$, for any $\psi$. Therefore $\psi^M$ holds for all $ZFC$ axioms).
Now, I claim that $M$ is self-relativizing. Indeed, $ZF\vdash AC^M$, so $ZF\vdash \phi(x)^M\leftrightarrow (x\in L)^M$. But $L^M$ is $M$ in both cases, because $M$ is either $L$ or $L^*$, and $L^*$ is isomorphic to $L$. Therefore, $ZF\vdash \phi(x)^M\leftrightarrow \phi(x)$.
Finally, $ZF$ cannot prove that $L\subseteq M$, and $ZF+\neg AC$ proves that $M$ is a proper sublass of $L$.
