exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated. With more work,

exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated. With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)