I'm still relatively new to formal specification but it seems that some form of weak/strong fairness would suffice for the correctness of your invariant and the

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