What TLA+ can and can't check
- ID
- 30842
- Status
- summarized
- Published
- 30 Sep 2026, 9:57 PM
- Fetched
- 02 Oct 2026, 12:26 AM
- Provider
- Hacker News
- Category
- dev-community
- Original URL
- https://buttondown.com/hillelwayne/archive/what-tla-can-and-cant-check/
- Source URL
- https://hnrss.org/best
Summary
- Score
- 7.0
- Created
- 02 Oct 2026, 12:27 AM
- Tags
- Audience
- developersvibe_codersai_agent_usersai_ml_learners
What happened
Hillel Wayne's Buttondown post What TLA+ can and can't check responds to Boris Cherny's claim that Opus used TLA+ to find race conditions in code, pushing back on the idea that formal methods will solve agentic software development. It walks through what TLA+ can express, including behaviors as state sequences, the temporal operators [] always, P' next, and <> eventually, plus invariants and action properties, while promising to focus on properties TLA+ cannot even express. The excerpt ends mid-explanation of action properties and stutter-invariance, and the Hacker News thread had 222 points and 47 comments.
Why it matters
If you use coding agents like Claude Code or Opus for bug-fixing, do not treat a TLA+ run as a turnkey correctness guarantee: the author notes you still need a property to verify, and correct designs do not automatically translate into correct code. Teams should decide who writes and reviews the invariants or properties before trusting agent-generated fixes.
Discussion angle
Opus reportedly used TLA+ to find race conditions, but who writes the property it checks? Discuss where human-specified invariants should fit into an agentic coding workflow.