What happens to provability of consistency if we restrict semantics to $\omega$-models? If we restrict the semantics of a first order theory to only $\omega$-models of it, then if a theory doesn't have an $\omega$-model, then its $\omega$-inconsistent, now an $\omega$-model only have standard naturals, and cannot satisfy sentences not satisfied by the standard model of arithmetic. Now if a theory $\sf T$ is $\omega$-consistent, then any $\omega$ model of it will not satisfy $\sf \neg Con(T)$, so it must satisfy $\sf Con(T)$. We are left with two options:

1- any theory $\sf T$ sufficient to express its consistency in its language, that is $\omega$-consistent, and if $\sf T^*$ is $\sf T$ semantically restricted to $\omega$-models of $\sf T$, then $\sf T^*\vdash \omega$-$\sf Con(T^*)$,

or

2- there is a sentence true in ALL acceptable models of $\sf T$, that is not syntactically captured by it?

Which sentence is true?
 A: This is a great question, but somewhat difficult to ask precisely. In my opinion things are made more difficult by bringing in the idea of syntactic entailment (= proof) too blithely. So let me be a bit more careful here:
Suppose we have a class $\mathbb{K}$ of structures. We can refine the usual entailment notion $\models$ between sentences to restrict attention to $\mathbb{K}$ as follows: $$\Gamma\models_\mathbb{K}\varphi\quad\iff\quad\forall\mathcal{M}\in\mathbb{K}(\mathcal{M}\models\Gamma\implies\mathcal{M}\models\varphi).$$ You can check a few basic properties of this notion. For example:

*

*If $\mathbb{K}$ consists of a single structure (up to isomorphism) $\mathcal{A}$ then $\Gamma\models_\mathbb{K}\varphi$ essentially reduces to the theory of that structure.


*More substantively, $\models_\mathbb{K}$ is not compact in general.
We can similarly restrict theories. Given a theory $T$ and a class of structures $\mathbb{K}$, let $$T^\mathbb{K}=\{\varphi:\forall\mathcal{M}\in\mathbb{K}(\mathcal{M}\models T\implies \mathcal{M}\models\varphi)\},$$ or using the notation above $T^\mathbb{K}=\{\varphi: T\models_\mathbb{K}\varphi\}$. Note that $T^\mathbb{K}$ is automatically deductively closed, so asking what $T^\mathbb{K}$ proves just amounts to asking what $T^\mathbb{K}$ contains. In particular, if $T=\mathsf{ZFC}$ (or similar) and $\mathbb{K}$ = $\{$$\omega$-models$\}$ then $T^\mathbb{K}\ni\mathsf{Con}(T)$ as you observe. This amounts to your option (1) ... but somewhat unsatisfyingly, since we've blatantly cheated in building $T^\mathbb{K}$ in the first place.
Can we do better?
Ideally, we would find a natural to tweak, not the theory $T$ itself, but rather the deduction relation $\vdash$ used to analyze it. Put another way, we want to understand:

Can we "algorithmically" (or "syntactically" or etc.) describe $\models_\mathbb{K}$ at least for certain choices of $\mathbb{K}$ (e.g. $\omega$-models)?

Note that the non-compactness of $\models_\mathbb{K}$ in general poses a problem here. At this point let's restrict attention to $\mathbb{K}$ = $\{\omega$-models$\}$.
(If I were being historically accurate I'd probably mention something about "$\omega$-logic" here, but that's not my preferred narrative line, so:)
It turns out that, necessary nonsenses of noncompactness notwithstanding, there is a very useful positive fact here:

There is a single sentence in the logic $\mathcal{L}_{\omega_1,\omega}$ which captures the class of $\omega$-models of (say) $\mathsf{KP}$. Moreover, $\mathcal{L}_{\omega_1,\omega}$ has a "surprisingly-nice-all-things-considered" proof system.

The first sentence of the above is a good exercise. The second sentence is a deep result of Barwise, the so-called Barwise completeness theorem. It's also been misstated for simplicity: really, every countable fragment of $\mathcal{L}_{\omega_1,\omega}$ (but not the whole!) has a good proof system in an appropriate sense. In particular, already the computable infinitary formulas are enough to do the job. Note that the special case of Barwise completeness that we need in this instance is also due to Kreisel (cf. the section in Ash/Knight's book on Barwise-Kreisel compactness).
I've avoided giving details here, since they're a bit technical, but the overall point I want to make here is that your case (1) can be construed as holding in a non-trivial way if we broaden our notion of proof a bit.
