Can we have reachability properties in TLA⁺?

[Andrew Helwer]

Surprisingly (or unsurprisingly, depending on how much of Lamport's writing you've read) the answer is yes! Reachability properties seem like more of a branching-time logic thing but they're viable in TLA+ with some fairness assumption trickery.

I found the way reachability properties work in TLA+ pretty hard to understand, so did my best to break it down in this post: https://ahelwer.ca/post/2026-09-26-reachability/

It could be possible to modify TLC to more easily express & check reachability properties. This could be useful for modeling eventually-consistent systems, where the property we care about is that different replicas must be able to converge to identical views of the system, not that they necessarily do converge.

Andrew Helwer