[tlaplus] About machine-closed Fairness Property

My question is: When writing a spec, is it our HUMAN's responsibility to make sure a WF or/and SF property is Machine-Closed, or the model-check runtime will help do the sanity check and point out: Hi, dude, the WF is NOT a subaction of the NEXT...?

I wrote a simple spec to test what gonna happen when a fairness action is not Machine-Closed. And seems to me the checker will NOT do sanity check and keep updating the state. I am not very sure if my testing case is correct or not, though.

------------------------------ MODULE Fairness ------------------------------
EXTENDS Naturals
VARIABLE x
FairnessIni == x=0
FairnessNext == x'=x+1

\*I tried to introduce an WF action that will break the NEXT safety property.
\*Please refer to Lamport's 2019 paper: Safeness, Liveness and Fairness

FairnessChaos == x'=x+2

\* Conjunction together with Init, Safety and WF property
Fairness == FairnessIni /\ [][FairnessNext]_x /\ WF_x(FairnessChaos)

\* Put a invariance check to see if the state x is growing...
Invariance == x <100
--------------------------------------------------------------
THEOREM Fairness => []Invariance

=======================================================================

Then I run the TLA+ model checker. Apparently, every time the state will go from 0 to 101, and then check! "Invariant Invariance is violated."