Specula · specula-org/Specula

Scaling formal specs for autonomous bug finding

Specula finds deep bugs in concurrent and distributed system code. It uses coding agents to write TLA+ specs of the target system, including invariants that capture the system's correctness properties and formal models that describe the system implementation. It then model-checks the specs and reproduces violations at the code level. Specula has been used to find deep bugs in many open-source projects. For more details, see our paper.

We maintain a list of bugs found by Specula. We would love to hear about the bugs you find using Specula.

Browse the case-study archive for reports, models, and reproduction evidence. The case-studies submodule pins the archive and its system and run indexes for this checkout.

Prerequisites

Python 3.10+ with pip
uv
Java 21+ with Maven
GitHub CLI gh
Supported agents (Claude Code, Codex, Copilot CLI, OpenCode, or Pi). Please contribute adapters for new agents.
Coding agent. (Specula uses coding agents to read code, infer invariants, and reason about counterexamples.)
Machine: We recommend at least 32 GB of RAM and 100 GB of free disk space; more RAM is preferable. See the Usage Guide.

Windows: run Specula inside WSL2. Native Windows (outside WSL2) is not supported yet.

Recommended Coding Agents

We recommend using the following coding agents, which we actively test:

Claude Code with Claude Opus 4.8 or Fable
Codex with GPT-5.5 or GPT-5.6-Sol

Other strong coding agents may work, but we do not test them regularly during our development. We recently tested Claude Code with GLM-5.2, Kimi 2.7, and DeepSeek V4 (see Usage Guide).

For GPT-5.6-Sol and Fable, apply for Trusted Access through OpenAI and Anthropic, respectively. Without the required access, providers may block bug-reproduction requests during confirmation. If you cannot obtain access, use hybrid configuration to select another agent or model for that phase.

Setup

git clone https://github.com/specula-org/Specula.git && cd Specula
uv tool install -e .   # installs the `specula` command
specula setup          # installs the agent skills and MCP tools, builds the bundled tools

Manual Setup

You need to set up the Specula Agent Skills and MCP with your coding agent.

Symlink the Specula skills directory to the one read by your coding agent, e.g., ~/.claude/skills or .claude/skills for Claude Code, ~/.codex/skills or .agents/skills for Codex, and .github/skills for Copilot CLI.
Add the trace_debugger, spec_analyzer, and inv_checking_tool MCP tools to your agent config. Please build the CFA tool with Maven before adding spec_analyzer.

# for trace debugger MCP
cd tools/trace_debugger
python3 -m venv .venv
. .venv/bin/activate
pip install -r requirements.txt
cd ../..  # return to the Specula repository root

# for Claude Code
claude mcp add --transport stdio --scope project \
    tracedebugger \
    --env "SPECULA_ROOT=$PWD" -- \
    "$PWD/tools/trace_debugger/.venv/bin/python" \
    "$PWD/tools/trace_debugger/mcp_server.py"

# for Codex
codex mcp add tracedebugger \
	--env "SPECULA_ROOT=$PWD" -- \
	"$PWD/tools/trace_debugger/.venv/bin/python" \
	"$PWD/tools/trace_debugger/mcp_server.py"

# for GitHub Copilot CLI 1.0.21+
copilot mcp add tracedebugger \
    --env "SPECULA_ROOT=$PWD" -- \
    "$PWD/tools/trace_debugger/.venv/bin/python" \
    "$PWD/tools/trace_debugger/mcp_server.py"

Automatic MCP configuration is skipped for older Copilot CLI versions; upgrade to the latest version to enable it.

Auto Mode

specula run mysys \
  --artifact=/path/to/repo \
  --guidance=/absolute/path/to/mysys-guidance.md

The mysys-guidance.md is optional but recommended. It is a configuration file that guides Specula to focus on target modules and scenarios, with consistent modeling scope across runs. We provide a template and an example.

Outputs are stored in runs/. After a run, start with runs/latest/pipeline-summary.md.

Add --keep-original to leave the source checkout untouched. Specula runs the same agents against a full private copy and writes a reviewable source diff to runs//mysys/changes.patch. Ignored build output is omitted, while binary and trace contents remain in the private source instead of being inlined. Specula does not apply the diff to the original checkout.

The detailed usage and configurations can be found in the Usage Guide.

Continuous Verification

Initialize a persistent model and harness, then check later source changes incrementally:

specula run --ci-init --ci-dir=/work/mysys-ci \
  --artifact=/path/to/repo --guidance=/path/to/mysys-guidance.md mysys
specula run --incremental --ci-dir=/work/mysys-ci

Keep the CI directory outside the source checkout. See Add Specula to CI for setup, results, and the GitHub Actions workflow. Existing TLA+ models and verification assets can be imported with Bring Your Own Model.

Interactive Mode

Open your coding agent in the Specula directory. The workflow is a sequence of skills, each producing input for the next:

code-analysis → spec-generation → harness-generation → validation-workflow → bug-confirmation

(Codex uses $code-analysis, $spec-generation, etc. after choosing y in specula setup, or $specula-codex:code-analysis, $specula-codex:spec-generation, etc. in plugin mode.)

To start, tell the agent your target and invoke the first skill:

This project is a Go implementation of Tendermint BFT consensus (cometbft/cometbft).
The reference algorithm is the Tendermint paper (arXiv:1807.04938). Run /code-analysis.

Each skill produces output files (e.g., modeling-brief.md, base.tla, traces) in .specula-output that the next skill will consume. When one skill completes, invoke the next. You can also run any skill independently, e.g., validation-workflow on an existing spec.

Changelog

See CHANGELOG.md for release history and notable changes.

Acknowledgement

We are grateful to the generous support from

TLA+ Foundation
OpenAI
Anthropic (AI for Science Program)
Qingrong Chen

License

Apache License 2.0.