I&#x27;m still relatively new to formal specification but it seems that some form of weak&#x2F;strong fairness would suffice for the correctness of your invariant and then it&#x27;s a matter of testing your liveness properties while holding the invariant with a model checker.<p>TLA+ seems pretty good at this. Why would this be a waste of effort?