Specula: LLM agent autonomously specs system code, finds 249 bugs

Specula, a new push-button agentic system developed by researchers at the University of British Columbia and the University of Illinois Urbana-Champaign, leverages large language models (LLMs) to generate high-quality formal specifications for complex system code. The system uses coding agents to autonomously develop TLA+ specifications, including invariants that define correctness properties and formal models that abstract implementations appropriately. By operating fully autonomously, Specula removes the traditional barrier of requiring human experts to write formal specifications, a process that has long limited the adoption of formal methods in real-world software engineering.

The system addresses key LLM limitations like reward hacking and hallucinations through self-evolving loops that iteratively improve specification quality. As agents deepen their understanding of the target system code, the specifications become more accurate and effective for model checking. In testing across 48 open-source system projects, Specula discovered 249 bugs, many of which are deep, subtle defects that existing approaches struggle to find. The system is already in use by several companies and is publicly maintained, signaling a practical step toward making formal verification accessible at scale for production software.