The Solovay inner model satisfies ZF and every real set has a real–ordinal definition

Hereditary definability makes $M$ transitive, contains every ordinal, and contains every real because a real is itself an $S$-parameter; Extensionality, Foundation, Pairing, Union and Infinity are therefore inherited.

Separation is obtained by conjoining the defining formula of the separated class with the fixed $OD(S)$ definitions of its set parameters. For Replacement, if $f,x\in M$ and $f$ is functional on $x$, the ambient set $f\mathrm{‘}\mathrm{‘}x$ is defined from the fixed hereditary codes of $f$ and $x$ by $y\in f\mathrm{‘}\mathrm{‘}x⟺(\mathrm{\exists }z\in x)(z,y)\in f$; every such $y$ is already in the transitive class $M$, so the image is hereditarily $OD(S)$ and belongs to $M$. No per-value codes are selected or combined. For Power Set, the ambient set $\{y\subseteq x:y\in M\}$ is defined from $x$ by the uniform $OD(S)$ predicate, and all members of its transitive closure lie in $M$. Thus every ZF axiom holds in $M$.

Let $A\subseteq \mathbb{R}$ lie in $M$. Heredity gives a definition of $A$ from $s\in S$ and finitely many ordinals $\vec{\alpha }$. By F2, $s$ lies in a bounded initial extension. The real-capture clause of F3 supplies a real $r$ and ordinal $\beta$ such that $s$ is definable over $V[r]$ from $(r,\beta )$. By F4, $V[r]=L[r]$. The class $L[r]$ is uniformly definable in $V[G]$ from $r$, so syntactically restricting every quantifier in the fixed defining formula to $L[r]$ defines the same unique $s$ in $V[G]$. Substitute that ambient definition of $s$ into the definition of $A$. Thus $A$ is definable in $V[G]$ from $r$ and the finite ordinal tuple $(\beta ,\vec{\alpha })$. Conversely, interleave the natural-number bits of $r$ and the finite tuple $(\beta ,\vec{\alpha })$ into one countable ordinal sequence in $S$. Hence the advertised parameter forms are equivalent, without claiming that an arbitrary ordinal is real-coded or that $M=L(\mathbb{R})$.