Can we have reachability properties in TLA⁺?

# Can we have reachability properties in TLA⁺? Source: [https://ahelwer.ca/post/2026-09-26-reachability/](https://ahelwer.ca/post/2026-09-26-reachability/) I was reading Hillel Wayne’s new post[*TLA\+ Won’t Solve Everything*](https://www.linkedin.com/pulse/tla-wont-solve-everything-hillel-wayne-3edyc/)and became fixated on one of the things he says cannot be expressed in TLA⁺: > Possibility and reachability properties: that it’s always possible to make P true, even if you don’t actually decide to\. Things like “I can always shut down the computer” or “A user can always change their password”\. These can’t be expressed with <\>P because that’s “for all behaviors, P happens at least once”, we actually want “for all behavior prefixes, there is at least one behavior where P happens at least once”\. This made me think\. A while back I was reading Lamport’s new book,[*A Science of Concurrent Programs*](https://lamport.azurewebsites.net/tla/science-book.html), and was doing pretty well until getting completely shut down by section 5\.1,*Possibility and Accuracy*\. The section talks about this exact topic, expressing possibility/reachability properties in TLA⁺\. I could not wrap my head around it, to the point I thought there were major errors in the text\. Hillel’s post spurred me to revisit it[1](https://ahelwer.ca/post/2026-09-26-reachability/#fn:1), and I am happy to say I now basically understand it and will try to explain it in a way that makes sense to me\. If you’d rather have it explained to you by Lamport directly, read section 5\.1 of the above textbook or Lamport’s October 1998 paper[*Proving Possibility Properties*](https://lamport.azurewebsites.net/pubs/lamport-possibility.pdf)\. We will go over two questions: 1. Is it possible to model\-check reachability properties in TLA⁺ using TLC, the finite\-state model checker? \(Yes, definitely, but not without changing TLC\) 2. Are reachability properties actually kosher by TLA⁺ semantics, or some kind of hideous intrusion of branching\-time logic into the linear\-time logic of TLA? \(It’s fine, suprisingly\!\) ## TLA⁺ already has reachability \- kind of\! One of the more prominent \(and weird[2](https://ahelwer.ca/post/2026-09-26-reachability/#fn:2)\) operators in TLA⁺ is`ENABLED`\.`ENABLED A`evaluates to true in a given state if action`A`can be taken in that state\. The most common application of it is to check`\[\]ENABLED Next`\. This just says that it is always possible for your system to take another non\-stuttering step\. If this ever becomes false, your system is deadlocked\! A very useful property, so much so that TLC checks it by default\.[3](https://ahelwer.ca/post/2026-09-26-reachability/#fn:3) `ENABLED`also lets you write the most basic reachability property, which is asking whether it is possible to reach a state in a*single step*\. The property`\[\]\(ENABLED Next /\\ P'\)`checks that you can always reach state`P`within a single step\. TLC will check this today\. However, it isn’t very useful\. We usually want to know whether`P`can be reached in*multiple*steps\. Lamport defines another operator, which he writes using the plus\-superscript character`⁺`\.[4](https://ahelwer.ca/post/2026-09-26-reachability/#fn:4)Its meaning will be familiar to anybody who knows regular expressions: it means one or more actions can be concatenated together\. Lamport thus expresses full reachability properties as`\[\]\(ENABLED \[Next\]\_v^\+ /\\ P'\)`, meaning one or more`Next`steps \(or stuttering\) can be taken to reach`P`instead of just one\. This is quite an ugly formula written in ASCII; here it is all gussed up: $$ \\Box\\text\{E\}\(\[Next\]\_v^\+ \\land P^\{\\prime\}\) $$ TLC*cannot*currently check this property; it exists only as a figment in Lamport’s imagination\. It also looks suspiciously like branching\-time logic\. Heresy\! More on this later\. ## What TLC can and could check Beyond`ENABLED`, TLC recently added support for[basic reachability properties](https://github.com/tlaplus/tlaplus/pull/1377)\. These are still in beta, so you have to declare them in your model file as`\_POSSIBLE P`\. This does not check reachability from every system state; instead, it checks whether`P`can*ever*be satisfied at all, by any behavior starting in one of the initial states\. You can read the motivation[here](https://github.com/tlaplus/tlaplus/issues/860#issue-2075413374), which is mostly about functioning as a “unit test” for your spec[5](https://ahelwer.ca/post/2026-09-26-reachability/#fn:5)\. Checking`\_POSSIBLE`is straightforward in TLC’s regular breadth\-first search: if`P`is never hit by the time state exploration terminates, then report a failure\. It was also[recently figured out](https://github.com/tlaplus/tlaplus/issues/860#issuecomment-5655381578)that`\_POSSIBLE`offers a more ergonomic way of expressing trace validation, so it seems likely to stick around in the language\. What about full possibility/reachability properties? Can we check that`P`is reachable from*every*system state? TLC*could*certainly check those, but it would take more work\. Thankfully this work has the shape of adding an additional isolated pass to model\-checking instead of intertwining itself with existing machinery, so it could be viable to implement with limited risk of breaking things\. The algorithm to use is called*backward reachability*\. After the full state graph has been explored, write a pass that does breadth\-first search on the state graph in*reverse*, starting from every state satisfying`P`and proceeding through every state that transitions*to*those states\. If you have any unexplored states left over at the end, you know`P`isn’t reachable from those states so report a violation\. Those leftover states even give a nice counterexample to start debugging\! Whether this will ever be implemented in TLC is unknown, but it seems like not a bad idea\. ## Sneaking in branching\-time reasoning Here I’ll do my best to explain the trick Lamport cooked up to get something that looks like branching\-time reasoning into a linear\-time logic\. Just to forewarn, this section will be substantially more technical than the others\. The semantics of TLA⁺ fundamentally define a specification as a set of infinite linear behaviors\. This set of behaviors is itself generally infinite[6](https://ahelwer.ca/post/2026-09-26-reachability/#fn:6)\. So within this infinite set of infinite linear behaviors, what could we possibly mean when we say`REACHABLE P`? Conventionally, TLA⁺ formulas have to apply to*every*behavior in this set\. But we aren’t interested in whether every behavior actually reaches`P`; we want to know whether every behavior*could have*reached`P`\! This kind of speculative future reasoning is entirely at home in branching\-time logic but alien to linear\-time logic\. The fundamental trick is to abuse fairness assumptions\. A fairness assumption is a predicate you can use to filter the set of behaviors\. For an example of common usage, a system that just sits there not doing anything \(stuttering forever\) is a perfectly valid behavior of a conventional TLA⁺ specification, but it isn’t very interesting\. Thus many specs, if they want to check liveness properties like “eventually the system reaches a goal state”, will disallow those uninteresting behaviors with a fairness assumption like “if an action is continually enabled, it must eventually be taken”\. Informally, I like to think of fairness assumptions as adding ocean currents to your specification that broadly nudge it toward desired states\. Your system can still run around the entire state space, but it can’t get stuck somewhere forever without the current pushing it toward more productive behavior\. Fairness assumptions are usually how you encode the “happy path” of your system like how sending a network message eventually succeeds, that kind of thing\. A fairness assumption is*machine\-closed*if it does not keep the system from rejecting finite behaviors, only infinite ones \- like rejecting the behavior that sits there stuttering and doing nothing forever[7](https://ahelwer.ca/post/2026-09-26-reachability/#fn:7)\. More formally stated, every finite system behavior prefix*must*be extensible in a way that satisfies your fairness assumption, if your fairness assumption is machine\-closed\. In non\-gibberish, this means that at any given moment in a behavior, it can wake up and be like “oh shoot, I forgot I need to satisfy the fairness assumption\!” and then it can take a bunch of actions and go do that\. The behavior can never reach a point after a finite series of steps where it’s beyond redemption\. You may have noticed this “finite prefix must be extensible in a way that satisfies something” language looks a bit like talking about speculative future execution\! And that’s the key to it all\. Suppose you want to check whether state \\\(P\\\) is reachable from every possible system state\. If this were true, then some subset of system behaviors will include state \\\(P\\\)\. In fact, a subset will include \\\(P\\\) infinitely many times\. In TLA⁺\-ese, they satisfy the formula \\\(\\Box \\Diamond P\\\)[8](https://ahelwer.ca/post/2026-09-26-reachability/#fn:8)\. What if you could then write a machine\-closed fairness assumption \\\(F\\\) which admits only a very restrictive set of system traces, all of which satisfy \\\(\\Box \\Diamond P\\\)? Then, by the definition of machine closure, every finite prefix of the specification can be extended to satisfy \\\(\\Box \\Diamond P\\\)[9](https://ahelwer.ca/post/2026-09-26-reachability/#fn:9)\. Thus every finite prefix admitted by the specification can reach \\\(P\\\)\! Semantically valid reachability properties in TLA⁺\! Written as: $$ \(Spec \\space \\land \\space F\) \\Rarr \\Box \\Diamond P $$ So we have reduced the problem of stating “is \\\(P\\\) reachable by all states” to finding a suitable fairness assumption\. Skeptical readers might rightfully believe I have stuffed quite a bit into that detail\. Like sure if some magical fairness assumption drops out of the sky that is 1\. machine\-closed, and 2\. somehow uniquely picks out traces satisfying \\\(\\Box \\Diamond P\\\) then I guess this works\. But what reason do we have to believe that such a fairness assumption exists? And how could we actually derive it in reality for some arbitrary specification? ## Constructing a fairness assumption First we should give people an opportunity to bail out here\. If all you care about is model\-checking finite\-state systems for reachability, we’ve shown that reachability probabilities work in linear\-time logic\! It isn’t some unmendable rupture in TLA⁺ semantics to talk about reachability\. Go bother the TLA⁺ mailing list about adding reachability checking to TLC\. The rest of this section will only appeal to the weirdos who want to formally prove things about infinite\-state systems\. To reiterate, if you want to prove that a spec satisfies reachability property \\\(P\\\), it suffices to derive a machine\-closed fairness assumption \\\(F\\\) such that: $$ \(Spec \\space \\land \\space F\) \\Rarr \\Box \\Diamond P $$ There is a generalized existence construction for \\\(F\\\) given in Lamport’s[*Proving Possibility Properties*](https://lamport.azurewebsites.net/pubs/lamport-possibility.pdf), so if \\\(P\\\) actually*is*reachable then a suitable fairness assumption must exist, but there isn’t a way to derive \\\(F\\\) mechanically in a way that makes it easy to reason about in proofs; it requires creativity\! Let’s work on an example\. Consider a spec of a single variable, \\\(x\\\), serving as a counter that can either increment or decrement: $$ Up ≜ x^\{\\prime\} = x \+ 1 $$ $$ Down ≜ \(x \> 0\) \\land x^\{\\prime\} = x \- 1 $$ $$ Next ≜ Up \\lor Down $$ $$ Spec ≜ \(x = 1\) \\land \\Box\[Next\]\_x $$ Suppose we want to prove that \\\(x = 0\\\) is always reachable, which of course it is\. What fairness assumption \\\(F\\\) can we come up with which is both machine\-closed and ensures \\\(\\Box \\Diamond \(x = 0\)\\\)? Our first attempt might be to play it safe & familiar with \\\(F = SF\_x\(Down\)\\\)\. Any fairness assumption composed of conjunctions of weak or strong fairness of sub\-actions of \\\(Next\\\) will always be machine\-closed\. However, this is insufficient\. The behavior that takes two \\\(Up\\\) steps for every one \\\(Down\\\) steps satisfies this \\\(F\\\), while never reaching \\\(x = 0\\\): $$ 1 \\rightarrow 2 \\rightarrow 3 \\rightarrow 2 \\rightarrow 3 \\rightarrow 4 \\rightarrow 3 \\rightarrow 4 \\rightarrow 5 \\rightarrow \\ldots $$ It must be accepted that we have to abandon the usual safe ways of constructing machine\-closed fairness assumptions and give trust to our own ability to prove that a potential formula is machine\-closed\. A good second attempt along this new line of attack is \\\(F = \\Diamond \\Box \[Down\]\_x\\\): at a certain point the behavior says damn it all and only ever decrements\. This is promising\! If it only ever decrements, then it will head monotonically toward \\\(x = 0\\\)\! It’s also machine\-closed, since any behavior can stop at any point and just start decrementing\. Unfortunately this fails because it allows perpetual stuttering: $$ 1 \\rightarrow 1 \\rightarrow 1 \\rightarrow 1 \\rightarrow 1 \\rightarrow \\ldots $$ The fix is simple and familiar: conjoin it with weak fairness of \\\(Down\\\): $$ F = \\Diamond \\Box \[Down\]\_x \\land WF\_x\(Down\) $$ This is also machine\-closed, and it certainly ensures \\\(\\Box \\Diamond \(x = 0\)\\\)\. So we’ve done it\! We can use conventional liveness proof techniques[10](https://ahelwer.ca/post/2026-09-26-reachability/#fn:10)to prove the reachability of \\\(x = 0\\\) from every state\. Actually our example is suggestive of a broader pattern\. For defining \\\(F\\\) for an arbitrary spec, a decent starting point has the form: $$ F = \\Diamond \\Box \[A\]\_v \\land SF\_v\(A\) $$ Where \\\(A\\\) is an action \(not necessarily an exact sub\-action of \\\(Next\\\)\) which would bring every state in the system closer to \\\(P\\\)\. So any behavior can at any point drop everything and head directly toward \\\(P\\\)\. The particulars will, of course, depend on your spec\. ## Applications to eventual consistency In a[previous post](https://ahelwer.ca/post/2023-11-01-tla-finite-monotonic/), I wrote a model of an eventually\-consistent system \(a conflict\-free replicated datatype\)\. Eventually\-consistent systems have the property that each replica will always be slightly out of sync with the others, but if transactions stop flowing then all replicas are guaranteed to eventually converge to the same view of the system\. I didn’t realize it at the time, but this is a reachability property\! We want the system to always be*able*to converge, not that it necessarily always will\! I ended up expressing this in a clumsy way by having an artificial boolean flag which could trigger at any time to stop new transactions, then checked that when the flag was true the system eventually converged\. Now armed with the above knowledge of expressing reachability properties in TLA⁺, the flag could have been a fairness assumption instead\! Something like this was actually[suggested at the time](https://github.com/tlaplus/Examples/pull/97#discussion_r1802130732), although I did not understand it then\. So actually TLC*does*support checking reachability properties now, as long as the user expresses them in the \\\(\(Spec \\space \\land \\space F\) \\Rarr \\Box \\Diamond P\\\) formalism\! Quite a tall order, since I with my decade\-plus of TLA⁺ experience didn’t understand that method until writing this very blog post\. Implementing reachability checking in TLC as its own thing with a backward reachability pass would be a tremendous improvement in usability\. ## Discussion - [lobste\.rs](https://lobste.rs/s/8pjbtj/can_we_have_reachability_properties_tla) - [Mastodon](https://discuss.systems/@ahelwer/117338159798722923) - [LinkedIn](https://www.linkedin.com/feed/update/urn:li:activity:7509641393628262400/) - [Hacker News](https://news.ycombinator.com/item?id=49857717) - [TLA⁺ mailing list](http://discuss.tlapl.us/msg06817.html)