Is there a computable ordinal encoding the proof strength of ZF? Is it knowable?

Rom Maimon is describing the program of proof-theoretic ordinal analysis.

First, as you observed in your addendum, it isn't interesting to find some encoding of an ordinal whose well-foundedness implies Con(ZFC), but rather an ordinal such that the well-foundedness of any representation implies Con(ZFC). One hopes that it suffices to consider natural representations of the ordinal, which has been true in practice, but is unproven (and probably unprovable, given the difficulty of making precise what counts as a natural representation).

It's possible to prove that the smallest ordinal which ZFC fails to prove well-founded is computable by noticing that the computable notations for ordinals provably well-founded in ZFC are a $\Sigma_1$ subset of the computable notations for ordinals, so certainly $\Sigma^1_1$, and by a result of Spector, any $\Sigma_1^1$ subset of the computable notations for ordinals is bounded.

As pointed out in the answer Timothy Chow links to above, it's typically true that this notion of proof-theoretic ordinal ends up being the same as ordinals with other nice properties (like implying Con(ZFC)), but there's no proof that that will always happen (and can't be, since there are defective examples that show it's not always true), nor a proof that covers ZFC.

However it's generally believed that for "natural" theories, including ZFC, the different notions of proof-theoretic ordinal will line up.

Finding an explicit description of the ordinal for ZFC is an active problem in proof theory, but progress has been very slow. The best known results are by Rathjen and Arai (separately) at the level of $\Pi^1_2$-comprehension (a subtheory of second order arithmetic, so much, much weaker than ZFC), and after nearly 20 years, those remain unpublished. The results in the area got extremely difficult and technical, and didn't seem to provide insight into the theories the way the smaller ordinals had, so it's not nearly as active an area as it once was. Wolfram Pohlers and his students still seem to working in the area, and some other people seem to be thinking about other approaches rather than directly attacking it (Tim Carlson and Andreas Weiermann and their students come to mind).

For every c.e. theory T (extending a weak base theory), we already know a polynomial time computable linear ordering $≺$ that captures the $Π^1_1$ strength of T:
Provably in a weak base theory, a $Π^1_1$ statement is provable in T iff for some term s, it is provable in a weak base theory plus "$≺$ is well-founded below s".
Thus, for $Π^1_1$ sound T, the order type of $≺$ is the supremum of order types of provably-in-T recursive well-orderings, and $≺$ is a well-ordering iff T is $Π^1_1$ sound.

Here is an example of $≺$:
$(p_1,q_1,n_1) ≺ (p_2,q_2,n_2)$ if $(p_1,q_1)<(p_2,q_2)$ (lexicographically)
$(p,q,n_1) ≺ (p,q,n_2)$ iff
- $q$ is a T-proof that bounded-time Turing machine $p$ computes a well-ordering, and $p$ accepts $(n_1,n_2)$ (any reasonable choice for 'bounded time' that keeps $≺$ polynomial time works here), or
- $q$ is not a T-proof of the above, and $n_1<n_2$.

The problem is that the above $≺$ is uninformative about T. A key goal of ordinal analysis is to find a canonical $≺$ that makes the power of T simple and explicit, and thus give us a qualitatively better understanding of T. Existence of a noncanonical $≺$, combined with existence of canonical $≺$ for weaker theories, suggests that a canonical $≺$ also exists for ZFC, but it is difficult to be certain until we actually find and prove such a $≺$. Typically, an approach to finding $≺$ can be extended until it becomes too complex, and then a new idea permits $≺$ to become simpler again.

A caution about ordinal representations:
* Every sufficiently large recursive ordinal has different recursive representations that are not arithmetically isomorphic.
* I think that for every recursive ordinal α and a c.e. theory T (extending a base theory), there is a recursive representation $≺$ of α such that T + "$≺$ is well founded" is $Σ^1_1$ conservative over T. This follows from existence of a recursive pseudowellordering $≺_p$ such that T + "$≺_p$ is well founded" is $Σ^1_1$ conservative over T.