The internet discovers TLA+. Now what?

A viral tweet by Boris Cherny about using TLA+ (Temporal Logic of Actions) for formal modeling in AI-powered coding has renewed interest in this 30-year-old formal verification toolkit. The article explains that while TLA+ is useful for describing system behaviors and properties, true verification requires combining it with modern proof systems and AI agents to move seamlessly between specifications, proofs, and actual code implementation. Reasonable, the company behind the post, is developing agentic pipelines that automate this process, having already converted thousands of TLA+ specification pairs into machine-checked proofs.