specula-org / Specula

Specula: A framework for finding deep bugs in system code using TLA+ Specula is an AI-powered framework that uses TLA+ formal specification to find bugs in system code. Specula uses LLMs to accelerate formal modeling, from code analysis to specification generation to trace validation, significantly reducing the cost and effort of formal specification and verification of system code. We have been applying Specula to find deep bugs in distributed system code. See the running list of bugs found by Specula. Overview Specula is a multi-phase agentic workflow. Each phase is driven by a dedicated skill that encodes knowledge and methodology and is materialized by a coding agent. • **Code Analysis.** The agent statically analyzes the target codebase with the following actions: (1) understanding core modules, (2) mining Git history and GitHub issues, (3) comparing the code against the reference paper and reference systems (if any) to detect deviations, (4) grouping its findings based on “bug families”, and (5) producing a _modeling brief_ that guide specification generation. • **Specification.** The agent translates the modeling brief into the following four specifications: (1) a TLA+ model that conforms to the control flow of the target code, (2) a model-checking specification with counter-bounded actions, (3) a trace-validation specification, and (4) a specification for code instrumentation. • **Trace Validation and Model Checking.** The agent alternates the following tasks: • **Trace Validation** — Verifying that the model can reproduce every state transition observed in a real execution trace, catching model-code gaps before model checking. • **Model Checking** — Exploring the state space to find invariant violations and analyzing counterexamples to determine if they are code bugs, model bugs, or known issues. Quick Start Specula runs as a set of code agent skills and MCP tools. It currently supports Claude Code and Codex, with more agents to be supported in the future. Prerequisites • A supported code agent (Claude Code or Codex) installed • Java 21+ (for TLC model checker) Setup Alternative: Manual Agent Setup You will need to set up the Specula Agent Skills and MCP with your coding agent. • To set up skills, symlink the Specula folder to the appropriate folder read by your coding agent. For Claude, this is or . For Codex, this is or . • To set up the MCP, add the MCP here to your agent config. Running Specula The case study name will be the directory name in the subdir (i.e. ). For example, if is cloned into : **Full pipeline** (all three phases): See here for more CLI options (e.g. specifying which agent to use) **Individual phases:** Note Specula has evolved significantly over the past months. Specula-v1 was a four-step code-to-model synthesis tool (which is archived). License See LICENSE for details.