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.
Why it matters
Agents finding race conditions with TLA+ has sparked claims that formal methods will fix agentic coding. This piece explains that you must first express the property, and which properties TLA+ cannot state, so you can set realistic expectations.
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