Proving What's Possible
This title could be clearer and more informative.Try out Clickbait Shieldfor free (5 uses left this month).
Formal methods consultant Hillel Wayne explores a third class of temporal properties beyond safety (A) and liveness (E): possibility properties (P), which express whether something *can* happen in a system model. P(x) asks if x is reachable at some future point, enabling combinations like A(P(x)) — x is always possible no matter the current state. A key practical use is as a spec sanity check: verifying that a state like 'Retry' is actually reachable, preventing trivially-true liveness properties. While tools like TLA+ and Alloy don't natively support P, simple reachability can be mimicked by checking that A(!x) finds a counterexample. More complex combined operators like A(P(x)) cannot be mimicked this way, and the author notes a chicken-and-egg problem: lack of tooling means practitioners rarely notice when possibility properties matter.
