Search papers, labs, and topics across Lattice.
Specula is an autonomous system that generates formal specifications for complex system code, utilizing large language model (LLM) coding agents to create TLA+ specifications and invariants that capture correctness properties. This approach not only streamlines the application of formal methods to real-world systems but also addresses common pitfalls of LLMs, such as reward hacking and hallucinations, through iterative self-improvement loops. In testing across 48 open-source projects, Specula identified 249 bugs, including many that traditional methods struggle to detect, showcasing its effectiveness in enhancing software reliability.
Specula uncovers deep bugs in system code that traditional methods often miss, revolutionizing formal specification generation.
Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code and uses the specifications for highly effective model checking and bug finding. Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications, including invariants that describe correctness properties of the target system and formal models that describe the system implementation with the right level of abstractions. Specula is fully autonomous and thus eliminates the barrier of applying formal methods to real-world system code (as in traditional human-centric approaches). Meanwhile, Specula addresses limitations of LLM-driven techniques like reward hacking and hallucinations through self-evolving loops that iteratively improve specification quality by enabling the agents to deepen their understanding of system code and its behaviors. We have used Specula to check 48 open-source system projects; Specula found 249 bugs including many deep bugs that are hard to find by existing approaches. Specula has been used by several companies and is maintained at https://github.com/specula-org/Specula.
Microsoft Research