Formal verification starts with a precise statement of what software must do. In Hillel Wayne's explanation of TLA+, the language can express rules such as allowing at most one traffic light to be green or requiring machines eventually to agree on a leader.
Other questions fit less naturally. Comparing energy consumption across two alternative executions, for example, requires reasoning about both executions together. Wayne describes modeling workarounds and specialized tools, each with tradeoffs. For AI-generated software, the consequence is that choosing and expressing the right property remains essential: a successful check establishes the specified property, not every quality someone might want.
Terms in this piece · Glossary
LLM — A large language model — the neural network behind tools like Claude and ChatGPT, trained on huge amounts of text to predict what comes next.
AI agent — An AI system that doesn't just answer once but works toward a goal in a loop — taking actions, reading the results, and deciding what to do next.
articleFormal methods with Hillel Wayne (The Pragmatic Engineer Podcast)Gergely Orosz
articleTLA-Prover: Verifiable TLA+ Specification Synthesis via Preference-Optimized Low-Rank AdaptationEric Spencer, Arslan Bisharat, Brian Ortiz, Khushboo Bhadauria, Mujtaba Nazari, TaiNing Wang, George K. Thiruvathukal, Konstantin Laufer, Mohammed Abuhamad
articleWhen Code Becomes an LLM Call: An Empirical Study of Call-Site Contracts in Agentic SystemsShihao Weng, Longtian Wang, Yang Feng, Mingfei Cheng, Jia Liu, Chao Shen, He Ye, Federica Sarro, Xiaofei Xie