TLA+ hype returns after Opus race-condition find; educator details what it can't check

Formal verification is having an unsolicited moment in the spotlight. According to a newsletter post by Hillel Wayne, a long-time TLA+ educator and advocate, the trigger was a recent remark from Boris Cherny, the inventor of Claude Code, that Opus was able to use TLA+ to find race conditions in code. That claim set off a wave of online discussion about formal methods, and Wayne's counterweight post — which surfaced on Hacker News's front page — has become the reference point for what the language actually covers.

Wayne writes that the attention is exciting for a tool he has spent years promoting, but that the accompanying euphoria worries him. He rejects outright the idea, now circulating online, that formal methods will settle the problem of agentic software development once and for all. Rather than repeat the familiar caveat that a verified design does not automatically produce correct code, he focuses on a subtler boundary: before you can verify a property, you need a property the language can express at all.

What TLA+ checks

TLA+ models a system as a collection of behaviors, each behavior being a sequence of states. Ordinary boolean statements about a single state — say, that every traffic light is red — combine with three temporal operators: one meaning a property holds now and in every future state, one meaning it holds in the very next state, and one meaning it holds now or at some point later. Checking an always-property across every behavior yields an invariant, the workhorse of TLA+ verification. Wrapping next-state operators inside an always produces action properties, such as a value that never decreases. Both are safety properties — roughly, guarantees that nothing bad ever happens. Liveness properties, built on the eventually operator, assert that something good does happen: that nodes eventually agree after a leader election, that an algorithm eventually terminates with correct results, or that one condition eventually leads to another. Per Wayne, invariants, action properties, liveness and refinement account for the overwhelming majority of what people actually check.

The properties it cannot express

Wayne sorts the blind spots into several groups.

First, anything you cannot formalize. If a requirement cannot be written as a logical formula — his example is proving an app recognizes birds — no formal method can help.

Second, multi-step and timed claims. TLA+ safety properties speak about single states or single transitions, so you cannot natively state that pressing delete and then undo restores the original state, or that a computer turns on within ten steps of the power button. Floating-point operations and real time are also out of scope; the logic sees only logical time.

Third, reachability. Because properties are implicitly quantified over all behaviors, there is no way to assert that some behavior exists — that a game is winnable, or that a given state is reachable from every start.

Fourth, hyperproperties, which range over sets of behaviors. Verifying that a phone's energy-saving mode always draws less power than normal mode requires comparing two executions, something a single-behavior logic cannot express. Wayne notes that many security properties and all statistical properties, such as a 95th-percentile response time, sit in this bucket.

Finally, metaproperties about the state space as a whole, such as there being exactly one path between two states — though Wayne admits he is unsure how useful those would prove in practice.

Workarounds, with costs

None of these limits is absolute. Wayne describes encoding a running history of states in an auxiliary variable to fake two-step properties, and self-composition — where each behavior of an inflated spec bundles two behaviors of the real system — to approximate some hyperproperties. The TLC model checker now offers a REACHABLE keyword for basic reachability questions and a TLCGet mechanism for some state-space queries, and Andrew Helwer has written about emulating always-reachable behavior using fairness and machine closure.

But Wayne frames all of these as hacks. Each takes considerable cleverness to construct, auxiliary variables break refinement, self-composition blows up the state space exponentially, and the techniques do not compose well with the rest of the toolkit.

Why it matters

If agents like Opus can genuinely drive TLA+, design-level verification becomes far more accessible, and race-condition hunting is precisely the kind of problem the language was built for. But the boundary matters as much as the capability. TLA+ checks what can be expressed as a property of every behavior, in logical time, at the level of a specification — and a verified spec is still not verified code. Teams sold on the idea that formal methods will neutralize the risks of AI-written software will hit these walls quickly. The honest pitch, per Wayne, is narrower and more durable: a powerful tool for designing complex concurrent systems correctly, working alongside — not instead of — every other assurance technique.