What TLA+, Quint, Lean, and Rocq can and cannot verify

On 24 September 2026, Hillel Wayne, a developer educator at Antithesis who wrote the book Practical TLA+ and the free guide Learn TLA+, posted a response to what he described as euphoria about Opus 5.5's skill with TLA+, and to the idea that all software will soon be formally verified. He praised what TLA+ does well, especially finding concurrency bugs, then wrote that “there's a lot it fundamentally can't do,” and that the same goes for every other formal verification language.

That matters to anyone running a software factory. In SWFT's terms, the proof loop is where an agent checks its own work before the work advances, and a model-checked specification is a demanding check to put there. Agents already write some of these specs: by March 2026, Hillel reported that 4% of TLA+ specs on GitHub mention the word “Claude” somewhere. What a passing check covers is as narrow as it was before, and a leader signing off on a “verified” claim needs to know how narrow that is.

A spec describes behaviors of a design

TLA+ models a system as a set of behaviors: every possible sequence of states the system could pass through. Hillel's example is a program that picks a random number from 1 to 3 and counts down to 1. It has three behaviors: 3 → 2 → 1, 2 → 1, and 1.

A realistic spec for a checkout service would describe carts, payments, retries, and failures. The model checker, a program called TLC, explores every reachable state of a small instance of that design, such as two customers and three payment attempts, and prints the steps to any behavior that breaks a property.

Two facts follow. First, the spec models a design and is written separately from the code. The Learn TLA+ FAQ puts it directly: “TLA+ tests designs, not code.” Second, a property is a logical formula checked against each behavior on its own. Hillel's post describes the constraint in three parts: define a logical formula, apply it to individual behaviors, and check that every behavior satisfies it. Anything that cannot be written that way cannot be checked, however skilled the agent writing the spec.

Two property shapes: always and eventually

[]P, read “always P,” means P is true in every state of every behavior. This is an invariant. Hillel's examples are “your data is never corrupt” and “there's always at least one server online.” In a product: no account balance ever goes negative, and no seat is ever sold twice.

<>P, read “eventually P,” means P becomes true at some point in every behavior. Combined with “always,” it expresses the progress a system owes its users. <>[]P says the system eventually settles into P, as when an algorithm converges on the right answer. []<>P says P keeps coming back, as when data stores that drift apart always resync. [](P => <>Q) says every P is eventually followed by Q, as when every message put on a queue is eventually processed. In a product: every paid order is eventually shipped or refunded.

Hillel's essay on safety and liveness gives the distinction behind these shapes. Safety properties say a bad thing never happens, and a finite trace can prove them broken: here are the steps after which the balance went negative. Liveness properties say a good thing eventually happens, and only a behavior that never gets there can break them, such as a crash, an endless loop, or a deadlock in which no step is possible, which TLC also reports as an error of its own.

Two consequences matter when you review a spec an agent wrote.

Invariants alone can pass for a system that does nothing. A checkout that never processes an order never ships a wrong one. Hillel's rule is that most system properties are safety properties, but every system needs some liveness properties, or there was no reason to build it.

Liveness depends on fairness. TLA+ allows any system to stop taking steps forever, which is how it models a crash, so no liveness property can hold unless the spec adds fairness assumptions. Weak fairness says that an action that stays possible will, in time, happen. Strong fairness says the same of an action that keeps becoming possible, even if it is not possible the whole time. Fairness is a claim about the world, such as the scheduler keeps running the worker or the retry timer fires. Learn TLA+ warns against making a user process fair, because the user can always log off. Each assumption also narrows the result. In a May 2026 newsletter, Hillel showed that “any assumption added makes a property weaker”: the claim shrinks from the system has the property to if the assumption holds, the system has the property.

Five kinds of property a passing check does not cover

Hillel's post lists four categories TLA+ cannot express, then names a fifth as the core problem. Each has a partial workaround, and none of the workarounds closes the gap.

Possibility: “A user can always change their password”

This requirement says that from any point, there is some way to change the password, even if the user never does. Hillel's post pairs it with “I can always shut down the computer” and explains why <>P cannot express either: “eventually P” would require the password change to actually happen in every behavior. The requirement needs something different: from every point, at least one way forward leads to a changed password. TLA+ properties only speak about all behaviors.

The limit shows up in daily use through guarded properties. In a February 2026 newsletter, Hillel describes checking that a worker in a Retry state eventually leaves it. The check passes trivially if no worker can ever reach Retry. An agent-written spec full of if X, then Y properties can come back green because X never happens.

The workarounds each cover part of the gap:

• An invariant that must fail. Assert Retry never happens and expect a counterexample. Hillel notes that this shows one state is reachable from some starting state, one condition per run. It cannot show reachability from every starting state, or that something stays possible.
• Possibility conditions in newer TLC builds. TLC's 1.8.0 pre-release builds add a _POSSIBLE setting that fails the run unless each listed condition holds in at least one reachable state or step. The feature is provisional, and it shows only that the condition can occur somewhere, not that it stays possible from every point. Quint's --witnesses option counts how many simulated traces satisfy each listed condition, which is evidence from sampling rather than an exhaustive check.
• Liveness under fairness. Proving that the user eventually changes the password is a stronger claim than possibility, and it usually requires assuming the user is fair, which is false.
• A different logic. Computation tree logic, or CTL, reasons over branching futures and can state from every reachable state, recovery is possible. The NuSMV model checker analyzes CTL specifications, and Hillel writes that reachability is a regular, trivially checkable property in CTL. The cost is a second tool with its own language and limits.

Comparisons between runs: “painting a car red doesn't make it faster”

A hyperproperty is defined over two or more behaviors at once. Hillel's post gives two examples: painting a car red doesn't make it faster, and users cannot infer secret data by observing public data. No single run can break the car property. You need a red run and an otherwise identical run to compare. The same holds for determinism (the same inputs give the same result whatever the thread timing) and for this optimization returns the same answers as the old code. TLA+ looks at one behavior at a time, so it cannot state any of these.

The standard workaround is self-composition: a new spec that runs two copies of the original side by side and compares them with an ordinary property. Hillel's hyperproperties essay shows the technique and its limit: it works only for k-safety properties, where a counterexample is a fixed number of runs. It is also expensive. In his state-graph experiment, the regular model had 755 distinct states and the two-copy model had over 100,000. His September post calls this kind of lifting “insanely inefficient” and warns that the clever spec drifts away from the real system.

The practical tools here are tests that run code more than once per case, such as property-based tests that compare two implementations, differential tests, and metamorphic tests. Hillel's essay argues that tests suit relationships between calls for this reason.

Statistics: “95% latency is 1ms”

A frequency claim says how often something happens. Hillel's shorthand describes a latency percentile: 95% of requests finish within 1 millisecond. The Learn TLA+ FAQ states the limit: you can say X definitely happens or never happens, but not that X happens at least 90% of the time. Hillel's post adds that most statistical properties are hyperproperties. A spec's nondeterministic choice, such as the network may drop this message, is a possibility, not a probability.

Probabilistic model checkers exist for this job. PRISM analyzes Markov chains and related models with questions such as “what is the probability of a failure causing the system to shut down within 4 hours?” Models must be finite-state machines with explicit probabilities or rates, and Hillel notes that PRISM can't handle tuples or strings. The answer is only as good as the failure and arrival rates you assume. Marc Brooker and Ankush Desai of Amazon Web Services (AWS) describe extending TLC with probabilistic simulation to estimate latency distributions, which is simulation evidence rather than proof. Latency and uptime targets need load tests and production measurements.

Robustness to code changes

A result covers the behaviors of the artifact that was checked. Hillel's post gives the reason in one line: after a code change, you have new behaviors. His hyperproperties essay counts “Was this a safe refactoring” as a hyperproperty, because it compares two versions of the code. His newsletter on how verified code goes wrong adds that environmental assumptions, such as a vendor's API format, can change after code is proven and deployed, so verification cannot be one-and-done.

The remedies are procedural: rerun the checker or prover whenever the spec or the modeled code changes. For refactors, Hillel's cross-branch testing uses a property test whose property is that the refactored code gives the same output as the deployed branch.

Properties nobody can write as a formula

This is the largest category. Hillel's post states the rule: if we don't know how to express a property as a logical formula, we can't verify it, and “99% of the properties we care about fall under this.” His examples: information on a site is easy for a user to find, our LLMs behave as we expect, and an application can't be used to break the law. On these, he writes, TLA+ “(and Quint and Lean and Rocq) are near-useless here, no matter how clever you are.”

Hillel's own project shows how this goes wrong. Let's Prove Leftpad collects formally verified versions of leftpad, a function that pads a string to a given width. As he explains, the proofs show that the output's length is the target width, or the input's length if that is longer. Users want output that lines up on screen, and some Unicode strings padded to the right length don't line up. The proofs were valid. The property was a proxy.

Informal properties need other evidence: usability research for findability, evals and red-teaming for model behavior, legal review for compliance, and monitoring in production. A team may formalize a narrow proxy if it labels the proxy as one. For agent systems, SWFT's reading is that the deterministic harness around a model, such as the tool-call protocol, the retry and approval state machine, and budget stop rules, fits TLA+ or Quint. Whether the model's output is good remains an eval question.

The properties side by side

What each tool checks

The four tools Hillel names fall into two families. Model checkers, including TLC and Apalache for TLA+ specs and Quint's own tooling, explore the behaviors of a design automatically within bounds you choose. Proof assistants, including Lean, Rocq, and TLA+'s own proof system, check proofs that hold for all inputs with no bound, at much higher human effort. All of them share the limits above. Hillel adds that the other formalisms he names, CTL and PRISM, bring their own trade-offs, and that no single system can do everything.

TLA+: TLC, Apalache, and TLAPS

TLC checks every reachable state of one finite instance of a design, chosen by setting constants such as three nodes and two clients. Instances stay small because state counts grow fast: in one Learn TLA+ example, widening the input range would take the checker from about 70,000 states to over 500,000,000, by Hillel's estimate. A TLC result always comes with an instance attached, and its settings deserve scrutiny. A state constraint, for example, makes the checker skip states that violate it rather than report them.

The checker's version is part of the result. In February 2026, a TLC bug was reported that could produce both missed violations and bogus ones, and the issue traces it back to at least 2011. Its fix is in the rolling 1.8.0 pre-release, which the project's README says is rebuilt from every commit to the main branch. The latest stable release, v1.7.4 from August 2024, does not include it.

Apalache, according to the Quint CLI documentation, uses bounded model checking: it checks all runs up to a maximum number of steps, 10 by default when called from Quint. The same documentation describes a mode for inductive invariants, which hold for runs of any length once the base case and the step check both pass. TLAPS, the TLA+ Proof System, sends proof steps to automatic backends such as the Z3 solver, but a person or an agent still writes the proof structure.

Quint

The Quint FAQ describes Quint as based on TLA+, using the same underlying logic restricted to a fragment of it, so a Quint spec can be translated to TLA+. It adds types and a syntax closer to mainstream programming. The FAQ states the trade: TLA+ is more expressive in theory and has a proof system, which Quint does not.

quint run is random simulation. Its documented defaults are 10,000 samples of at most 20 steps, and its --invariant option defaults to true, so a run that names no invariant checks nothing. quint verify runs Apalache by default, or TLC with --backend tlc. A passing quint run is a sampled result and should be reported as one. Quint's link to code is model-based testing: it writes traces from the model to files, and a test driver replays them against the implementation. Quint Connect, a Rust library for this, launched in December 2025.

Lean

Lean is an open-source programming language and proof assistant. A small kernel checks each proof, and the result holds for all inputs. Lean fits pure functions, parsers, policy engines, and algorithms.

Two limits matter for a team accepting Lean proofs from agents. First, a Lean theorem is about Lean definitions, and it speaks for production code in another language only through a link someone builds. AWS's Cedar policy language shows one pattern: according to the Lean project's account, the team writes executable Lean models about 10 times smaller than the production Rust, proves properties of the models, and runs millions of random inputs through both to check that they agree. Aeneas translates safe Rust into Lean and other provers, and lists unsafe code and concurrency as future work.

Second, a proof is only as good as what it trusts. Lean lets an author skip a step with sorry or declare an axiom, and the Lean reference describes #print axioms as the way to find them: if sorryAx appears, the theorem or one of its dependencies is incomplete. The kernel can also have bugs. In July and August 2026, OpenAI researcher Daniel Selsam, working with the Lean team, used an internal OpenAI model to find soundness bugs in Lean's kernel and runtime, and Lean v4.33.1 fixed them. The postmortem notes that a normal build does not protect users from adversarial proofs and points to independent checkers for that case.

Rocq

Rocq is the proof assistant formerly called Coq; version 9.0, released on 12 March 2025, completed the rename. It gives the same class of guarantee as Lean, with the same gap to code in other languages. The reasons to choose it are specific. Iris, a framework for reasoning about concurrent programs, is implemented and verified in Rocq. CompCert, a C compiler with a machine-checked proof that the generated code behaves as the source program's semantics prescribe, is built with it. Like several other provers, Rocq can extract a verified program into ordinary code. A team already using Lean has little reason to add a second proof assistant unless it needs one of those.

Practical complements

Four everyday methods cover much of what the formal tools leave open:

• Property-based testing generates many inputs and checks a stated property against each, as Hypothesis does for Python. It is cheap and handles comparisons between runs well, but proves nothing about untried inputs. Hillel argues that thorough testing and review often give very high confidence more cheaply than a full proof.
• Deterministic simulation testing runs the real system on a simulator that controls scheduling, timing, and message order. Brooker and Desai describe it as widely used at AWS, and TigerBeetle's simulator can reproduce any bug it finds from a seed number and a Git commit.
• Evals test AI behavior on realistic work with explicit criteria, which is where a property like “Our LLMs behave as we expect them to” belongs.
• Monitoring checks production against the properties that matter. AWS's PObserve, for example, checks structured logs from testing and production against a formal specification written in the P language.

Where the spec and the code part ways

Nothing connects a TLA+ or Quint spec to the code unless a team builds the connection. The spec pays off anyway. Hillel's argument is that with a checked design, a production bug is either an implementation error or a broken assumption. Without one, it might also be a flaw in the design itself, which he calls the most dangerous kind and the most expensive to fix. He also explains why teams rarely keep the two fully in sync: a spec that can generate code or be proven against it loses much of the abstraction that made it short and useful.

Teams narrow the gap in four ways, each with a cost:

1. Generate tests from the model. MongoDB engineers dumped the TLC state graph for aspects of the operational transformation algorithm in Realm Sync and, as Hillel summarizes it, turned it into about 5,000 tests. Their paper calls test generation highly successful for Realm Sync, and Hillel notes that the component was low-level and deterministic, so the spec could stay close to the code. Quint's quint run --mbt writes traces for the same purpose.
2. Check recorded executions against the model. Trace validation instruments the code, records what it does, and asks the checker whether each recording is an allowed behavior. Researchers who applied it to several distributed programs found discrepancies between specification and implementation in every case. The MongoDB paper found trace checking impractical for its server, whose specification was highly abstract, and Hillel wrote in 2025 that trace validation takes a lot of manual work tailored to each product.
3. Prove the code itself. Lean with Aeneas, the Cedar pattern of proofs plus differential testing, or Rocq with extraction. This gives the strongest link and costs the most expert time.
4. Test the real code under faults. Deterministic simulation can use the spec's invariants as its pass-fail checks. Brooker and Desai write that the most important use of formal methods at AWS may be formal specifications serving as test oracles, which supply the correct answers for many of its testing practices.

Assumptions need the same scrutiny. If production loses, duplicates, or reorders messages, a spec whose network is perfectly reliable checks a system that does not exist.

What changes when agents write the spec

Hillel's June 2025 summary was that agents handled the tedious, routine parts of TLA+, such as fixing syntax errors, filling in boilerplate, explaining long error traces, and turning a precisely described property into TLA+, better than the strategic and abstraction parts. The limits above stay where they were, along with the gap to code and the human judgment about what to model and which properties matter.

Hillel's March 2026 review of beginner agent-written specs found recurring failures:

• Specs that don't run. One Alloy spec he examined did not compile, and he regularly sees agent-written TLA+ specs he doubts would model-check at all.
• Properties that cannot fail. In one TLA+ spec, a property named NoExploitAllowed required that whenever a gadget was detected, the decision was "block". The action that detected a gadget also set the decision to "block" in the same step, so the property restated the action. He found agents writing only “obvious properties,” which fail for reasons like a missed guard, rather than subtle ones that fail through concurrency, nondeterminism, or bad behavior several steps apart. The subtle properties, he writes, are where the value of formal methods lies.
• Liveness is hard to get. He and a client could not get an agent to produce a good liveness or action property even with explicit instructions.

His 2025 experiments found a fourth pattern. When the checker found a race condition, the agent often proposed declaring race conditions acceptable, or adding a constraint that races don't happen. His response to the first: “if you say bugs are okay, then the spec finds that bugs are okay!” He added that the spec needs to describe the mechanism that is supposed to prevent the race.

SWFT's reading is that this last pattern belongs in how a factory designs its proof loop. The spec's properties are the oracle that decides whether work passes. An agent rewarded for a green check that can edit both the code and the properties can reach green by weakening the check. The authors of ImpossibleBench, a benchmark that measures how often agents pass tasks that can only be passed by breaking the specification, give the example of an agent deleting failing tests instead of fixing the bug. Spec properties need the same protection as tests.

A checklist for teams whose agents write specs

1. Make each property fail on purpose. Remove the lock, guard, or version check a property depends on, predict the counterexample, and run the checker. A property that still passes does not check that mechanism. As Learn TLA+ notes, passing invariants look the same as having no invariants.
2. Show that the interesting states happen. For each if X, then Y or X leads to Y property, add a check that X is reachable: an invariant expected to fail, a _POSSIBLE condition on TLC builds that support it, or Quint's --witnesses.
3. Require progress properties. Wherever the system must make progress, such as queues, retries, leases, and approvals, require at least one liveness property. Tie each fairness assumption to a real mechanism, and do not assume fairness for users, operators, or attackers, who make no promise to act.
4. Write down what is out of scope. List the property kinds the spec cannot cover, the bounds that were checked (constants, step limits, simulation or exhaustive search), and the environment assumptions (network, clocks, crashes).
5. Review the oracle separately from the code. Changes to properties, constraints, assumptions, fairness, and theorem statements need a human reviewer apart from the code change. Fail the build when the number of checked properties drops without approval.
6. Name the claim at its true level. Say “model-checked design” rather than “formally verified system” unless the code itself is verified. A useful claim names the component, properties, bounds, tool version, and commit, for example: “The lease protocol design was model-checked with TLC against four safety properties and one liveness property, for three nodes and two clients. The service is tested against traces generated from that model. The run log records the tool version and commit.”
7. Pin tool versions. Record the checker or prover version and a checksum of the tool, because the TLA+ pre-release is rebuilt on every commit. Pin the Lean toolchain, and pin Quint and Apalache together. When you upgrade, rerun existing specs and compare verdicts.
8. Tie the model to the code. Generate tests from the model, validate recorded traces against it, or use its invariants as the pass-fail checks in deterministic simulation.
9. Rerun on every relevant change. Run the checker in continuous integration whenever the spec or the code it models changes, and use cross-branch tests for refactors.
10. Check what a proof trusts. Fail Lean builds that contain sorry, review the output of #print axioms for each headline theorem, and use independent proof checkers when agents write the proofs.