TLA+ hype check: what formal verification actually covers
Original: What TLA+ can and can't check
Why This Matters
As AI-generated code scales up, understanding the actual limits of verification tools matters more than the hype.
After Claude Opus reportedly used TLA+ to find race conditions, formal verification went viral. TLA+ educator Hillel Wayne pushes back: the tool can only verify properties you've already defined, and expressing every meaningful system property in TLA+ is harder than the hype suggests.
Boris Cherny, credited as the inventor of Claude Code, sparked widespread excitement last week by noting that Opus could use TLA+ to detect race conditions. The response online quickly escalated into claims that formal methods will 'solve' agentic software development. Hillel Wayne — a longtime TLA+ educator and advocate — welcomes the attention but flags a specific blind spot the conversation is missing.
TLA+ works by modeling system behaviors as sequences of states and checking temporal logic properties against them. Safety properties ('something bad never happens') and liveness properties ('something good eventually happens') are its bread and butter. Classic examples include invariants like 'at most one green light at a time,' action properties like 'x never decreases,' and liveness patterns like 'after a leader election, nodes eventually agree.'
Wayne's concern isn't about what TLA+ gets wrong — it's about what you have to supply first. To verify a property, you need to formally express that property. Many real-world correctness requirements are either too subtle to articulate precisely, too dependent on implementation details TLA+ doesn't model, or simply things engineers haven't thought to specify. A correct TLA+ model does not automatically mean correct code, and a passing spec check does not catch properties that were never written down.
The piece cautions against treating formal verification as a catch-all solution to AI-generated code reliability, calling that framing 'nonsense.'