Yes, the minimal transitive model of ZFC is pointwise definable. The minimal transitive model of ZFC, known as the [Shephardson-Cohen model](https://en.wikipedia.org/wiki/Minimal_model_(set_theory)), is the model $\langle L_\alpha,\in\rangle$, where the ordinal $\alpha$ is smallest such that this is a model of ZFC. Let me make a few observations about it. - The minimal model is not only minimal, but least. That is, if $M$ is any transitive model of ZFC, then the constructible universe $L^M$ of that model will also be a model of ZFC and have the form $L_\gamma$, and so the minimal model $L_\alpha$ will be contained within it. - It follows that the minimal transitive model of ZFC exists if and only if there is a transitive model of ZFC. - The minimal model might not exist — it is consistent with ZFC that there is no transitive model of ZFC. For example, in the minimal model $L_\alpha$ itself, there is no element that is a transitive model of ZFC. So it is consistent with ZFC that the minimal model does not exist. - The existence of the minimal transitive model of ZFC has some mild consistency strength. If there is a transitive model $M$ of ZFC, then of course Con(ZFC) must hold. But since the model is transitive, we get Con(ZFC) holding inside $M$, and so Con(ZFC+Con(ZFC)) holds. But then this holds also inside $M$, and so Con(ZFC+Con(ZFC+Con(ZFC))) holds, and so on. One can iterate this process transfinitely. So the existence of the minimal model implies a tower of iterated consistency statements transcending ZFC. **Theorem.** The minimal transitive model of ZFC is pointwise definable. **Proof.** Suppose that $L_\alpha$ is the minimal transitive model of ZFC. This model satisfies $V=L$ and consequently has a definable global well ordering of the universe. Using this, we see that there are definable Skolem functions. The set of definable elements of $L_\alpha$ is therefore closed under Skolem witnesses and is therefore an elementary substructure of $L_\alpha$. By condensation, this collection is isomorphic by the Mostowski collapse to a model $L_\beta$, which must be a model of ZFC, and which furthermore is pointwise definable, since we included only definable elements. Since $\beta\leq\alpha$, it follows by minimality that $\beta=\alpha$. And so $L_\alpha$ is pointwise definable. $\Box$ If one equips the minimal transitive model of ZFC with all its definable classes, then one achieves a minimal transitive model of Gödel-Bernays GBC set theory. Meanwhile, Kameryn Williams proved in his dissertation result that there is no minimal transitive model of Kelley-Morse set theory. - <cite authors="Williams, Kameryn J.">_Williams, Kameryn J._, [**Minimum models of second-order set theories**](http://dx.doi.org/10.1017/jsl.2019.27), J. Symb. Log. 84, No. 2, 589-620 (2019). [ZBL1453.03033](https://zbmath.org/?q=an:1453.03033).</cite>