# Proving What's Possible

DevFeed: [Proving What's Possible](<https://devfeed.tech/articles/proving-what-s-possible-25503.md>)

Original publisher: [Read original article](<https://buttondown.com/hillelwayne/archive/proving-whats-possible/>)

Author: Hillel Wayne

Published: 2026-02-11T18:36:53Z

Content type: opinion

Language: en

Sources: [Newsletter feed for Hillel Wayne's Newsletter](<https://devfeed.tech/sources/newsletter-feed-for-hillel-wayne-s-newsletter.md>)

Topics: [Formal methods](<https://devfeed.tech/topics/formal-methods.md>), [Specifications](<https://devfeed.tech/topics/specifications.md>), [Math and Logic](<https://devfeed.tech/topics/math-and-logic.md>), [systems](<https://devfeed.tech/topics/systems.md>)

Tags: [flow](<https://devfeed.tech/tags/flow.md>), [formal-methods](<https://devfeed.tech/tags/formal-methods.md>), [specifications](<https://devfeed.tech/tags/specifications.md>), [state](<https://devfeed.tech/tags/state.md>), [statement](<https://devfeed.tech/tags/statement.md>)

## AI overview

A formal methods consultant introduces possibility properties for reasoning about what can happen in a system, distinguishing them from safety and liveness properties. Using temporal-logic notation and examples involving databases and state machines, the article describes possibility and reachability properties and combinations such as always possible and eventually possible.

## Source excerpt

As a formal methods consultant I have to mathematically express properties of systems. I generally do this with two "temporal operators": A(x) means that x is always true. For example, a database table always satisfies all record-level constraints, and a state machine always makes valid transitions between states. If x is a statement about an individual state (as in the database but not state machine example), we further call it an invariant. E(x) means that x is "eventually" true, conventionally meaning "guaranteed true at some point in the future". A database transaction eventually completes or rolls back, a state machine eventually reaches the "done" state, etc. These come from linear temporal logic, which is the mainstream notation for expressing system properties. 1 We like these operators because they elegantly cover safety and liveness properties, and because we can combine them. A(E(x)) means x is true an infinite number of times, while A(x => E(y) means that x being true guarantees y true in the future. There's a third class of properties, that I will call possibility properties: P(x) is "can x happen in this model"? Is it possible for a table to have more than ten records? Can a state machine transition from "Done" to "Retry", even if it doesn't? Importantly, P(x) does not need to be possible immediately, just at some point in the future. It's possible to lose 100 dollars betting on slot machines, even if you only bet one dollar at a time. If x is a statement about an individual state, we can further call it a reachability property. I'm going to use the two interchangeably for flow. A(P(x)) says that x is always possible. No matter what we've done in our system, we can make x happen again. There's no way to do this with just A and E. Other meaningful combinations include: P(A(x)): there is a reachable state from which x is always true. A(x => P(y)): y is possible from any state where x is true. E(x && P(y)): There is always a future state where x is true a