Is there a model of ZF¬C where some program always terminates but has no loop variant?
I think you are really asking a question about the definition of the notion of well-foundedness.

I think the notion of loop variants is a bit of a red herring here: I would argue that any reasonable definition of well-foundedness should enable proving that a loop is terminating iff there is a well-founded relation which acts as a variant for it, almost as a tautology.

The issue is that the classical definition of a well-founded order $&lt;$ on $X$:


  There are no infinite sequences $x_1&gt;x_2&gt;x_3&gt;\ldots$


is not a very nice definition, either from a constructive standpoint or when one is uncomfortable with the use of the axiom of (dependent, thanks Andrej!) choice. Assuming the latter, this definition is equivalent to the much nicer definition:


  Every non-empty subset $P\subseteq X$ has a minimal element, that is, some $x\in P$ such that $y \not&lt; x$ for every $y\in P$.


This definition is already much nicer, and I think it can be used to prove the variant lemma without choice.

Finally, the constructive version of well-foundedness is this:


  For every $P\subseteq X$, if for every $x\in X$, $\{\ y\ |\ y &lt; x\ \}\subseteq P$ implies $x\in P$, then $P = X$.


This definition seems more unwieldy, but it is actually the one you want: it enables induction over well-founded orders, without using either choice or excluded middle. Assuming excluded middle, it is equivalent to the previous one.

Finally, the business in the wikipedia article about ordinals is not really necessary for any technical analysis of termination, and, in addition, choice is not required if you define $\omega_1$ to be the order type of the set of countable ordinals (ordered by the prefix relation).