Solution (source code)

= Solution

Suppose that the <countable ordinal> $\alpha$ satisfied $V_\alpha\models\mathsf{ZFC}$. The axioms force $\alpha$ to be a <limit ordinal> above $\omega$, so choose an externally countable <cofinal function> $n\mapsto\alpha_n$ into $\alpha$, with $\alpha_n+1<\alpha$. The internal <Axiom of choice> gives a <bijection> in $V_\alpha$ between each $V_{\alpha_n}$ and some ordinal below $\alpha$. Every such ordinal is externally a <countable set>, hence every $V_{\alpha_n}$ is externally countable. The <countable union of countable sets> is countable, so
$$
V_\alpha=\bigcup_{n<\omega}V_{\alpha_n}
$$
would be countable. But $V_\alpha$ contains the full <power set> $\mathcal P(\omega)$, which is uncountable by <Cantor theorem>. This contradiction is the result <Countable rank-initial segment cannot model ZFC>, and therefore
$$
\boxed{V_\alpha\not\models\mathsf{ZFC}.}
$$