Boris Cherny, inventor of Claude Code, recently demonstrated Opus using TLA+ to find race conditions — and the internet collectively decided formal verification would solve agentic AI. Hillel Wayne, a longtime TLA+ educator and advocate, is here to pump the brakes. Not on TLA+ itself, which he considers excellent for concurrent system design, but on the belief that formal methods can verify everything that matters. TLA+ operates on behaviors — sequences of states — and checks properties using three temporal operators: 'always' (□P), 'next' (P'), and 'eventually' (◇P). These compose into safety properties ('something bad never happens') and liveness properties ('something good eventually happens'). Invariants, action properties, and liveness cover a wide band of what engineers need. The system is genuinely powerful for what it does. But every TLA+ property is implicitly universally quantified over all behaviors. That single architectural constraint creates a hard wall. You cannot express 'there exists a behavior where P is true' — meaning reachability properties like 'this game is winnable' are out. You cannot define properties over pairs of behaviors — meaning hyperproperties like 'energy-saving mode always uses less power than normal mode' are inexpressible. Security properties and statistical properties (p95 latency, for instance) are hyperproperties. They're gone. The granularity problem is equally sharp. TLA+ safety properties work at single-state or single-step resolution. 'Pressing delete then undo restores the original state' requires two steps and cannot be natively expressed. Neither can real-time constraints, floating-point operations, or properties over the state space as a whole (like 'there's only one path from X to Y'). Workarounds exist — auxiliary variables that store state history, self-composition that pairs behaviors, TLC's new REACHABLE keyword. Wayne calls these 'useful hacks' and means it precisely: each one is clever, each one breaks something else. Auxiliary variables ruin refinements. Self-composition exponentiates state space. None compose cleanly with TLA+'s core features. The models become weird, messy, and stop corresponding to actual systems. Other tools cover different slices — CTL handles reachability, PRISM handles probabilistic properties — but each trades off against what TLA+ does well, and none handle properties that can't be expressed logically at all. If you can't formalize the human notion of a bird, no formal method proves your app recognizes birds. The bottom line is calibration. TLA+ picks a lot of low-hanging fruit in concurrent system correctness, and that fruit is genuinely valuable. But the current discourse — that AI agents plus formal verification equals solved software — misunderstands where the boundary sits. The limitation isn't tooling maturity. It's the expressive power of the logic itself. The things TLA+ can't check aren't bugs to be fixed; they're mathematical facts about what temporal logic over individual behaviors can say.
