TLA+ author Hillel Wayne pushes back on the idea that formal verification will save AI-written code
- Boris Cherny, the creator of Claude Code, said on X that Opus 5.5 formally verified the Claude Agent SDK with Lean, turning "a couple short prompts" into 16 PRs that fixed bugs and race conditions, and that he also combines Lean with TLA+ for data flow, concurrency, and state management. The post drew 5.6K likes and 487 replies.
- Hillel Wayne, who wrote Practical TLA+ and runs learntla.com, calls the new euphoria that formal methods will solve agentic software development "once and for all" nonsense, while saying he is glad the topic is getting attention.
- Wayne sets aside the familiar complaint that a correct design does not produce correct code and picks a different limit: before a tool can verify a property, someone has to express it, so he asks which properties TLA+ cannot even state.
- TLA+ splits a system into behaviors, each a sequence of states, and checks plain boolean expressions in each state through three temporal operators:
[]P(always),P'(next state), and<>P(eventually), with traffic lights as the running example. - Wayne's stated position is level-headedness: TLA+ is good at designing concurrent systems and finding bugs in them, and it is not a fix for the whole problem of letting agents write software.
Hacker News opinions
People keep saying we can just write tests, or more recently that we can point formal verification at it and hand the implementation to LLMs. Probabilistic guessing machines can't be the safeguard here. You still have to actually understand the thing you're building.
Part of this is a shortcoming of our programming languages. They let you express partial graphs, which makes verification technically hard. A language that only exposes closed-graph semantics could bridge the gap between the model and the implementation, even if it isn't absolute.
Found Quint through a comment on this thread. It's an executable specification language that works in JavaScript, with tooling built on the temporal logic of actions, so basically TLA. Anyone interested in TLA+ should check it out.
Worth remembering that formal methods can't prevent side channels in hardware and firmware that nobody verified. That's a different layer from what TLA+ is doing.
Floating point non-associativity and side channels are the classic examples of things formal methods shouldn't be expected to find. Not every bug is a state machine bug.