The internet discovers TLA+. Now what?

Blog The internet discovers TLA+. Now what? Boris Cherny’s viral TLA+ tweet showed how useful formal models can be in agentic coding. This post gives a practical introduction to what TLA+ is. But TLA+ is only the starting point. We also look at how temporal specifications, modern proof systems and AI agents can fit together, from modeling system behaviour to generating machine-checked proofs, and ...