The internet discovers TLA+. Now what?

By Anna Mészáros, Szilvia Ujváry, Kseniia Strelbytska, Balázs Szilágyi, and Ferenc Huszár

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 ultimately toward software that is specified, implemented and verified in one loop. We also give a sneak peek into some of our work at Reasonable on making this possible.