Can LLMs model real-world systems in TLA+? (www.sigops.org)

The Specula team recently explored the capabilities of Large Language Models (LLMs) in modeling system code using TLA+, a formal specification language for concurrent and distributed systems. They evaluated several leading LLMs, including Claude and GPT, by asking them to generate TLA+ specifications for complex systems like Etcd and ZooKeeper. The study revealed that while the LLMs excelled in syntax and runtime checks, they struggled significantly in accurately conforming to the specific behavior of the systems, often producing models that either misrepresented state transitions or relied on generalized formalization templates instead of adhering to the actual implementations. This research highlights the importance of moving beyond traditional evaluations that only assess syntax and runtime execution. By introducing SysMoBench, an automated benchmarking tool that examines LLM outputs across various phases—syntax, runtime, conformance, and invariance—the team aims to bridge the gap between textbook knowledge and real-world system representation. The findings call attention to the current limitations of LLMs in accurately modeling complex systems, indicating that while these models can generate syntactically correct code, aligning that code with real-world execution requires further refinement. The team is also working on enhancing SysMoBench and developing specialized agents like Specula, which show promise in achieving higher conformance and invariant scores.