Proving What's Possible

The article introduces possibility properties (P(x)) in formal methods, which indicate whether something can happen in a system model. These complement standard temporal operators A (always) and E (eventually), helping verify state reachability in specifications. However, mainstream formal tools like Alloy and TLA+ don't natively support possibility properties.