*This was previously [asked and bountied](https://math.stackexchange.com/questions/2326484/is-zfcv-l-consistently-omega-complete) on MSE:*

For brevity, let $T$ be $\mathsf{ZFC+V=L}$.

Say that an extension of $\mathsf{ZFC}$ is *$\omega$-complete* iff it has exactly one $\omega$-model up to elementary equivalence. While the $\omega$-incompleteness of $T$ is easily provable in theories only slightly stronger than $T$ itself, I don't immediately see how to do it in $T$ alone. My question is: 

> Is the theory $S:=T+$ "$T$ is $\omega$-complete" consistent?

Here are a couple observations:

 - If we replace "$\omega$-model" by "well-founded model," the answer is obviously **yes** under standard assumptions. Let $\alpha$ be the second-smallest ordinal such that $L_\alpha\models\mathsf{ZFC}$. Then $L_\alpha$ also satisfies "$\mathsf{ZFC+V=L}$ has exactly one well-founded model." Unfortunately, we have no analogous hierarchy of $\omega$-models, so this is a non-starter here.

 - As to the specific choice of theory in question, the point is that (something like) $\mathsf{V=L}$ is needed to block an easy proof of a negative answer via forcing. For example, reasoning in $\mathsf{ZFC}$, if $\mathsf{ZFC}$ had an $\omega$-model $\mathcal{M}$ it would have a countable one $\hat{\mathcal{M}}$, and we could force over $\hat{\mathcal{M}}$ to get a non-elementarily-equivalent $\omega$-model $\hat{\mathcal{N}}$. *(Forcing over ill-founded countable models is no harder really than forcing over well-founded ones.)* The key point here is that forcing preserves $\mathsf{ZFC}$. This breaks down of course for $\mathsf{V=L}$ and so this argument is irrelevant here. Given the paucity of techniques we currently have for building models of $\mathsf{ZFC}$ in the first place, this seems to be a real issue.

Ultimately I suspect that the answer is negative, but the above two points between them rule out all the lines of attack I've been able to think of so far.

****

EDIT: In light of Farmer S's answer below, let me explicitly mention a rule of thumb which I forgot: **when thinking about properties which are not too far from first-order definable, always consider the hyperarithmetic hierarchy!**

For example, for every $\mathcal{L}_{\omega_1,\omega}$-sentence $\varphi$, if $\varphi$ has a model then it has a model $M$ which is countable in $L$, and moreover the $L$-least (real coding a) model of $\varphi$ is hyperarithmetic relative to (any real coding) $\varphi$. The property "Is an $\omega$-model of $T$" is expressible as a computable $\mathcal{L}_{\omega_1,\omega}$-sentence, and this drives Farmer S's point that $T^+\in L_{\omega_1^{CK}}$.