This depends on how you define "proof-theoretic ordinal." I would say that to seriously address this question we need to restrict attention to a fully-objective definition (as opposed to one dependent on choice of notation; the answer then is that the proof-theoretic ordinal of an appropriate (= "does enough arithmetic") theory always exists, and all existing evidence points to it having the desired consistency-proving property (and so we expect the same to hold for ZF), but there is (to my knowledge) no metatheorem establishing that this in fact holds.

*In terms of how far ordinal analysis has been carried out in a way considered satisfying by the community (see the subtleties below), I believe the state-of-the-art is around $\Pi^1_2$-CA$_0$. My understanding is that ATR$_0$ represents the upper limit of the "relatively simple" analyses, and after that things get quite weird. But I'm not an expert.*

Related:

This paper by Rathjen is a good survey of general ordinal analysis.

I vaguely remember an excellent paper (by Avigad?) summarizing different definitions of proof-theoretic ordinal and analyzing their relationships; if I can find it, I'll add it.

This paper by Arai (and its sequel) isn't directly relevant, but looks at a different way to analyze (set) theories in terms of ordinals - focusing not on establishing consistency but on determining how complicated constructions the theory can establish. This approach is sufficiently "coarse" that it is quite feasible even at the level of ZF.

CAVEAT: Below I'm being a bit vague about what "proves induction along" means. In a theory in second-order arithmetic we can talk directly about well-orderedness; in a first-order theory we need to talk instead about fragments of induction (e.g. $\Sigma_1$-induction along the ordering in question).

A snappy definition you'll often see is indeed "The smallest ordinal such that induction along that ordinal proves (over PRA) the consistency of $T$." Of course this isn't really precise. Rather, we need to talk about ordinal *notations*: ignoring the details, these are just primitive recursive well-orderings of $\omega$ (ignoring the finite ones for now). Note that the set of actual notations is $\Pi^1_1$-complete.

The problem is that notations can be quite pathological. Consider for example the following way to build a linear order $\triangleleft$: we lay down points in order $$0\triangleleft 1\triangleleft 2\triangleleft ...$$ until we see a proof of $\perp$ in $T$, at which point we switch to building a copy of the "reversed" natural numbers. E.g. if the shortest proof of $\perp$ in $T$ has length $17$, we wind up building $$... 19\triangleleft 18\triangleleft 17\triangleleft 0\triangleleft 1\triangleleft 2\triangleleft 3\triangleleft ...\triangleleft 16.$$ There is a notation capturing this construction, and trivially induction along this notation proves (over PRA) the consistency of $T$. But its ordertype is just $\omega$ - **did we just prove that every (appropriate) theory has proof-theoretic ordinal $\omega$?**

No - when we say "induction along $\alpha$ proves the consistency of $T$," what we *really* mean is that there is some **natural system of unique notations** for ordinals up to $\alpha+1$ such that induction along the notation for $\alpha$ in this system proves (over PRA) the consistency of $T$, but induction along any smaller notation doesn't.

Of course **this is a fundamentally vague task**. In general though three other phenomena help motivate the specific choice:

The systems so produced tend to "cohere" - e.g. there's a "simple" translation according to which the system for ATR$_0$ extends the system for PA.

$T$ itself tends to (indeed, in every case I'm aware of does) prove induction along each smaller notation in that system.

The system itself emerges naturally from an analysis of proofs from $T$ (e.g. by looking at cut elimination processes).

By contrast, a fully notation-independent definition is the following:

The *computational* proof-theoretic ordinal $\vert T\vert_{comp}$ of $T$ is the supremum of the computable ordinals $\alpha$ such that there is some notation $n$ for $\alpha$ which $T$ proves is well-founded.

This makes sense for any (appropriate) theory $T$, and - so long as $T$ is sufficiently sound - is always striclty less than $\omega_1^{CK}$ (by $\Sigma^1_1$ bounding). It turns out that we have the following phenomenon:

For every "natural" theory $T$, there is a "natural" notation for $\vert T\vert_{comp}$ such that induction along that notation proves (over PRA) the consistency of $T$.

But as far as I know there is no meta-theorem which says that this will always be the case, and indeed I don't even know what such a theory would look like (you'd have to somehow pin down what a "reasonable" ordinal notation is). So while (as far as I know) this phenomenon is expected to hold for all natural theories, and in particular for ZF, that is open.

Another reasonable attempt at a "notation-independent" definition would be the following:

The *inevitable* proof-theoretic ordinal $\vert T\vert_{inev}$ is the least computable ordinal $\alpha$ such that for *every* notation $n$ for $\alpha$, induction along $n$ proves (over PRA) the consistency of $T$.

But it's not clear to me that such a thing exists in general. Indeed, even for PA I'm not sure if such a thing exists, let alone that it is $\epsilon_0$: why shouldn't there be useless notations for long ordinals?

**EDIT: Fedor Pakhomov pointed out below that Beklemishev showed that this ***never* exists.