Section 6.4 "Specifying Alternation: Liveness" in main.pdf of the TLA+ Hyperbook says:
Beginning the algorithm with --fair algorithm adds the fairness requirement WFvar(Next), which asserts:
3. The behavior does not end in a state sn if there exists a state sn+1 such
that the sequence s1 → ... → sn+1 also satisfies condition 2.
(Where condition 2 is "Each step si → si+1 of the behavior is a Next step")