In a previous MO question, I was told by several commenters that
(a) it's known that there exists a computable ordinal $\alpha_{ZF}$ that "encodes the strength of ZF set theory" (i.e., a least computable ordinal that ZF fails to prove is wellfounded), but
(b) at present, we lack any description whatsoever of a Turing machine computing $\alpha_{ZF}$.
This claim intrigued and surprised me, since it's rare that we can prove that a certain Turing machine exists, but only in a completely nonconstructive way.
Thinking about it further, though, it seems to me that we can give an explicit Turing machine that defines $\alpha_{ZF}$, of course under the assumption that ZF is sound. So I'd be grateful if anyone could tell me if I'm making a mistake in the following.
What we want, clearly, is the supremum of all the countablymany ordinals that ZF does prove to be wellfounded. But the following computer program, call it $P$, should compute the order relation of that limit ordinal:

Set $t:=0$. Loop over all possible derivations in ZF, searching for proofs of statements of the form, "the Turing machine $M$ computes the order relation of a wellfounded countable ordinal." Any time such a proof is found, set $t:=t+1$, and start up a parallel process labelled by $t$ (in "dovetailing" fashion) that simulates $M$, and that outputs "$\langle t,x \rangle < \langle t,y \rangle$" whenever $M$ outputs "$x < y$". Meanwhile, also define $\langle t,x \rangle < \langle u,y \rangle$ whenever $t<u$.
Assuming ZF is sound (at least in its claims about ordinal notations, if not its claims about transfinite sets), the output of $P$ should be the order relation of
$\alpha_1 + \alpha_2 + \cdots$,
where $\alpha_1, \alpha_2, \ldots$ is some enumeration (not necessarily in increasing order) of the ordinals that ZF proves to be wellfounded. But some simple ordinal arithmetic should then show that that ordinal is equal to $\alpha_{ZF}$, since the only thing that matters for determining its size is the fundamental sequence for $\alpha_{ZF}$ that it contains by definition.
Of course, if ZF is inconsistent, then $P$ will eventually output complete nonsense, while even if ZF is consistent but unsound, $P$ could output an order relation that fails to be wellfounded. In particular, the statement "$P$ defines a valid ordinal $\alpha_{ZF}$" implies Con(ZF), and hence can't be proved in ZF (assuming Con(ZF)). This is as we'd expect.
Now, if the above works, then it gives me a different understanding of the program of ordinal proof theorysomething I've been trying to learn a bit about from the extremelyknowledgeable Professor MO. In particular, it would mean that, when people ask for an "ordinal analysis of ZF," they're not asking for just any explicit description of the ordinal $\alpha_{ZF}$that's easy to get, by the above. Instead they're asking for a "combinatorial" description: a vague requirement, but one that basically means that our computer program describing the ordinal shouldn't make any direct reference to ZF itself. This way, one could imagine someone forming an intuition that $\alpha_{ZF}$ is wellfounded and therefore that ZF is consistent, without circularly presupposing Con(ZF) (as my program $P$ required us to do).