--- title: "What TLA+ Can and Can't Check: Limits of Formal Verification" description: "A practical look at TLA+ model checking boundaries: safety vs liveness, state-space explosion, and the properties TLA+ cannot even express, like reachability and hyperproperties." slug: "what-tla-can-and-can-t-check-limits-of-formal-verification" published: true read_time: 6 created_at: "2026-09-30 21:34:47.043 +0000 UTC" updated_at: "2026-09-30 21:34:47.046 +0000 UTC" author: "Typen" author_url: "https://typen.blog/@typen" tags: - "Featured" - "Backend" - "DevOps" - "Open Source" --- # What TLA+ Can and Can't Check: Limits of Formal Verification A practical look at TLA+ model checking boundaries: safety vs liveness, state-space explosion, and the properties TLA+ cannot even express, like reachability and hyperproperties. ![https://media.typen.blog/img/id/01a0f43d-d081-7120-b300-5c3974684ae6](trendbot-2658209996.webp) ## The Limits of a Powerful Tool TLA+ has a well-earned reputation for finding subtle bugs in concurrent systems. But enthusiasm for formal methods often outruns what the tools can actually do. Hillel Wayne, a long-time TLA+ educator and advocate, recently pushed back on the idea that formal methods will "solve" agentic software development once and for all. His argument is not that TLA+ is weak, but that its power is bounded in ways that are easy to overlook. One limitation gets discussed often: a correct design does not automatically translate into correct code. This article focuses on a different boundary. To verify a property, you first need to be able to express it. So what properties can TLA+ not even write down? ## What TLA+ Can Check TLA+ models a system as a set of behaviors. Each behavior is a sequence of states, like a traffic light going green, then yellow, then red. Within each state, you can write ordinary boolean expressions such as "light four is green" or "all lights are red." Three temporal operators extend those expressions: - `[]P` ("always P") holds if P is true now and in every future state. - `P'` ("P prime") holds if P is true in the next state. - `<>P` ("eventually P") holds if P is true now or in at least one future state. A property of the system is something true in the initial state of every behavior. Checking `[]P` therefore means P holds in every state of every behavior. This is an **invariant**, one of the most foundational properties in TLA+. Combining `[]` with primes gives **action properties**, such as `[](x' >= x)`, which says the new value of x is always at least the old value. Another useful form is `[](P => P')`: once P becomes true, it can never become false again. Invariants and action properties are both **safety properties**, roughly meaning "something bad never happens." **Liveness properties** are the other half: "something good always happens." They are built from `<>`. Alone, `<>P` is usually too weak, but composition yields more interesting statements: - `[]<>P` means P is true in at least one future state from every state. This can express recovery, such as nodes eventually agreeing on a leader after a new election. - `<>[]P` means P eventually becomes true and stays true forever. This is useful for showing algorithms terminate with the correct result. - `[](P => <>Q)` means every state where P holds is followed by a future state where Q holds. The sugar `P ~> Q` (P leads to Q) makes this easier to read. There are other operators, like `ENABLED` and `<>_v`, but most practical checking involves invariants, action properties, liveness, and refinement, which combines safety and liveness. ## What TLA+ Cannot Do ### Properties You Cannot Formalize The most obvious limit is also the most fundamental. If you cannot represent a property as a logical formula, no formal method can help. If you cannot formalize the human notion of a bird, you cannot prove your app recognizes birds. Many important properties fall into this category. ### Overly Specific Properties TLA+ safety properties operate at the level of individual states (invariants) or a single step (action properties). You cannot natively define a property over two or more steps, such as "pressing delete and then undo restores the original state" or "once power is pressed, the computer turns on within ten steps." TLA+ also cannot define properties over floating point operations or over real time, only logical time. ### Reachability TLA+ properties are implicitly quantified over all behaviors. Checking `[]P` really means "for all behaviors, `[]P` is true of that behavior's initial state." Every property TLA+ checks must hold for every individual behavior. That excludes statements of the form "there exists a behavior where P is true." In other words, TLA+ cannot say that P is possible, even if the system never reaches it. Proving a game is winnable is one example. These are called **reachability properties**. More advanced versions include "P is reachable from every initial state" or "P is reachable from any state where Q is true." ### Hyperproperties TLA+ also cannot define properties over a set of behaviors. These are **hyperproperties**. Suppose you are modeling phone hardware and want to verify that energy saving mode always uses less energy than normal mode. The property is: any sequence of actions uses no more power in energy saving mode than in regular mode. To refute it, you would need two behaviors that are identical except one starts in energy saving mode and the other does not, where regular mode uses less power. A single behavior is not enough, so this cannot be naturally checked in TLA+. Hyperproperties may sound niche, but they cover a large class of security properties and all statistical properties, such as "the 95th percentile response time is 5ms." ### State-Space Properties Finally, TLA+ cannot define properties over the state space as a whole. You cannot say, for example, that there is only one path from state X to Y. Whether this is useful in practice is less clear, but it is another category outside the language's reach. ## Workarounds and Their Costs The picture is more nuanced than a flat "TLA+ cannot do this." If your spec directly corresponds to the system you want to build, TLA+ cannot express these properties as properties of your system. But you can sometimes mimic them. Two-step properties can be approximated with **auxiliary variables**, such as storing all state changes in a `state_history` sequence and defining the property as an invariant over that sequence. Some hyperproperties can be mimicked with **self-composition**, where each behavior of the composed spec represents two behaviors of the actual system. The main TLA+ model checker, TLC, can check basic reachability with the `REACHABLE` keyword and some state-space properties with `TLCGet`. Andrew Helwer has written about mimicking "always reachable" using fairness and machine closure. These are useful hacks, but they remain hacks. Each requires cleverness and carries serious drawbacks. Auxiliary variables ruin refinements. Self-composition exponentiates the state space. Hacks do not compose well with other TLA+ features and do not cover all the intricacies of the properties you might want to express. Worst of all, they make models look weird and messy, and they stop corresponding to the actual system. ## Other Tools, Other Tradeoffs You could use a different tool with a different focus. CTL can handle reachability properties. PRISM handles probabilistic properties. Each trades off by being worse at things TLA+ does well, and none of them handle properties that cannot be expressed logically at all. ## The Practical Takeaway TLA+ is good at picking a lot of low-hanging fruit. Invariants and liveness cover many things we care about, and TLA+ expresses and checks them reasonably well. There is real potential in using it to check generated code, along with real pitfalls. But the boundary matters. There are many properties TLA+ cannot even express, let alone check. Treating formal verification as a universal solution to software correctness, especially in the context of agentic development, ignores those boundaries. The right question is not whether TLA+ can save us, but which properties we can state clearly enough for any tool to verify.