Explicit example of countable transitive model of $\sf ZF$ Do we know any explicit example of a countable transitive model for $\sf ZF$ or $\sf ZFC$?
 A: No. And yes.
$\sf ZF$, and by extension $\sf ZFC$, cannot prove their own consistency. Therefore within the confines of $\sf ZF(C)$ we cannot even prove that there are models of $\sf ZF$ to begin with.
Not only that. The statement "$\sf ZF(C)$ is consistent" is absolute between the universe and transitive models, so if there is a transitive model, not only that $\sf ZF(C)$, but also models of $\sf ZF+\operatorname{Con}(ZF)$ and much stronger theories.
So even if we assume the consistency of $\sf ZF$, we cannot prove that there are transitive models.
However! Just like $\Bbb N$ cannot be proved to exist just in $\sf PA$, we might as well take stronger theories instead of just $\sf ZFC$. And once a theory $T$, extending $\sf ZF$, proves that there exists a transitive model, then we know that there is a least $\alpha$ such that $L_\alpha$ is a model of $\sf ZFC$, and that $\alpha$ is countable. As far as explicit go, this is pretty damn explicit.
A: Asaf has given a great answer - let me give another answer which shows a sense in which the answer is no.
Given a theory $T$ (in a finite language to avoid silliness), we can ask if it has a computable model - that is, if there is a $\mathcal{A}$ which


*

*is a model of $T$, 

*has domain $\mathbb{N}$ (or a computable subset of $\mathbb{N}$), and

*all the relations and functions in the language are interpreted as computable relations and functions.
It turns out that ${\sf ZF}$ (indeed, much weaker than ${\sf ZF}$) has no computable models; see https://mathoverflow.net/questions/12426/is-there-a-computable-model-of-zfc.
The situation gets even worse for well-founded models: ${\sf ZF}$ has no hyperarithmetic well-founded models! "Hyperarithmetic" is a slightly technical definition, but basically anything you can define without using second-order logic is hyperarithmetic.
So I'd consider both these facts as good evidence that ${\sf ZF}$ (and, equally, ${\sf ZFC}$) has no "explicit" model.
