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$?

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.
