I mean, specific to my scenario, my invariant was "only one zone at a time" and the liveness property was "everyone who wants a zone eventually gets one", so re

I mean, specific to my scenario, my invariant was "only one zone at a time" and the liveness property was "everyone who wants a zone eventually gets one", so respectively: 1. \A z \in Zones: Active(z) => ~\E o \in Zones: z # o /\ Active(o) 2. \A w \in Workers: \A z \in Zones: WorkerWantsZone(w, z) ~> WorkerHasZone(w, z) Unlike your scenario, I am checking the spec here. I know that code that properly implements the spec satisfies these two properties, therefore I've proven the spec correct. You can disagree on the importance of those two properties but I've mechanically checked that those properties are always preserved in my finite models, so I know the spec is correct, at least for the model size. You know, it's really not too hard to get started with this stuff. You can always nit-pick but why not try it out and see if it's useful for you?