# Specula: Scaling formal specifications for autonomous model checking of system code

arXiv: https://arxiv.org/abs/2607.25333 · HTML: https://mlsanity.com/paper/2607.25333/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 31 of its 57 references that are in the map.
- First posted on arXiv 28 Jul 2026.

## Builds on (most cited first, 30 of 31)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Lost in the Middle: How Language Models Use Long Contexts](https://mlsanity.com/paper/2307.03172/) (2023)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering](https://mlsanity.com/paper/2405.15793/) (2024)
- [RULER: What's the Real Context Size of Your Long-Context Language Models?](https://mlsanity.com/paper/2404.06654/) (2024)
- [Scaling Laws for Reward Model Overoptimization](https://mlsanity.com/paper/2210.10760/) (2022)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [Hallucination is Inevitable: An Innate Limitation of Large Language Models](https://mlsanity.com/paper/2401.11817/) (2024)
- [The Effects of Reward Misspecification: Mapping and Mitigating Misaligned Models](https://mlsanity.com/paper/2201.03544/) (2022)
- [RepairAgent: An Autonomous, LLM-Based Agent for Program Repair](https://mlsanity.com/paper/2403.17134/) (2024)
- [Practical Program Repair in the Era of Large Pre-trained Language Models](https://mlsanity.com/paper/2210.14179/) (2022)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification](https://mlsanity.com/paper/2404.00762/) (2024)
- [SpecGen: Automated Generation of Formal Program Specifications via Large Language Models](https://mlsanity.com/paper/2401.08807/) (2024)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [DafnyPro: LLM-Assisted Automated Verification for Dafny Programs](https://mlsanity.com/paper/2601.05385/) (2026)
- [Agentic Verification of Software Systems](https://mlsanity.com/paper/2511.17330/) (2025)
- [FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning](https://mlsanity.com/paper/2604.11556/) (2026)
- [Validating Traces of Distributed Programs Against TLA+ Specifications](https://mlsanity.com/paper/2404.16075/) (2024)
- [KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code](https://mlsanity.com/paper/2605.03822/) (2026)
- [Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications](https://mlsanity.com/paper/2506.09550/) (2025)
- [The TLA+ Toolbox](https://mlsanity.com/paper/1912.10633/) (2019)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [Understanding Inconsistency in Azure Cosmos DB with TLA+](https://mlsanity.com/paper/2210.13661/) (2022)
- [Autobahn: Seamless high speed BFT](https://mlsanity.com/paper/2401.10369/) (2024)
- [Multi-Grained Specifications for Distributed System Model Checking and Verification](https://mlsanity.com/paper/2409.14301/) (2024)
- [Compositional Model Checking of Consensus Protocols Specified in TLA+ via Interaction-Preserving Abstraction](https://mlsanity.com/paper/2202.11385/) (2022)

## Abstract (arXiv)

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.