StackMap
Subscribe
Explore / Specula
specula-org

Specula

Agentic formal verification: coding agents write TLA+ specs and invariants of your distributed system, model-check them, and reproduce violations at code level. arXiv paper + public bug list.

338 36 Python Apache-2.0updated yesterday
coding
View on GitHubDispute this mapping →
Curator's take

The division of labor is right: the LLM writes the spec (the part humans never do), the model checker delivers ground truth (the part LLMs can't fake) — and the public spreadsheet of real bugs found in open-source systems is receipts most agentic tools don't have. When NOT: this is heavy machinery — Java+TLC, 32GB+ RAM, frontier agents (Opus/GPT-5.5 class) recommended; single-threaded CRUD code will never pay back the spec cost.

Mapped by ShipWithAI editors · links verified
README.md

specula

Scaling formal specs for autonomous bug finding

arXiv: 2607.25333 CI License: Apache 2.0

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.

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 reposit

Continue your stack

What teams reach for next — and why each earns a place beside Specula. Ranked by curator confidence.