# Specula: coding agents write TLA+ specs to hunt concurrency bugs

> Specula is a framework that has coding agents read a codebase, infer its correctness properties, write TLA+ specifications and formal models, model check them, and reproduce any violation back at the code level. It is Apache-2.0 licensed, needs a 32 GB machine and Java 21 for its model checker, and ships a list of the bugs it has found.

**specula-org/Specula** — Specula: An agentic tool for finding deep bugs in system code using TLA+

- Repository: https://github.com/specula-org/Specula
- Stars: 573 · Forks: 63
- Language: Python
- License: Apache-2.0
- Published: 2026-10-22 · Updated: 2026-10-22 · Language: en
- Canonical page: https://hysenlabs.com/projects/specula-org-specula

## The pipeline writes the spec, checks it, then reproduces the bug

Specula finds deep bugs in concurrent and distributed system code, and the mechanism is unusual enough to be worth stating precisely. 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. The middle step, writing the specification, is the one that distinguishes this from a model checker wrapper, because the properties a checker verifies are exactly the properties someone had to state, and stating them for a system you did not write is the expensive part. Specula asks a coding agent to infer the invariants from the code, and then uses a separate phase to reproduce a counterexample as something a developer can act on, which is the step that turns a formal result into a bug report. The project maintains a list of the bugs found by Specula and says it has been used to find deep bugs in many open-source projects, and there is a separate case-study archive repository with reports, models and reproduction evidence, pinned as a submodule. The research is written up in an arXiv paper, and the project is Apache-2.0 licensed with the primary language Python.

## What it needs before it will run

The prerequisites list is where the real cost of this approach is visible. You need Python 3.10 or newer with pip, uv, Java 21 or newer with Maven, the GitHub CLI, and one of the supported agents, with the README asking for adapters to be contributed for new ones. It also lists a coding agent separately, with the explanation that Specula uses coding agents to read code, infer invariants and reason about counterexamples. The machine requirement is the one to note, because it is well beyond a laptop. At least 32 GB of RAM and 100 GB of free disk space are recommended, with more RAM preferable. That figure is a consequence of the design rather than an accident, since a controller has to hold a model, a copy of the codebase, the traces it produces and the outputs of several agent phases at once, and the disk is where the traces and the run outputs land. Windows users are told to run Specula inside WSL2, because native Windows is not supported yet. The project is Apache-2.0 licensed and the release history shows steady work, with v1.2.0 on 2026-09-16, v1.1.0 on 2026-08-13 and v1.0.0 on 2026-08-01, and the last push to the repository on 2026-10-09.

## Setup installs the command and then wires the agent to the tools

The automatic setup is three commands.

```bash
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
```

The manual setup is the same thing spelled out, and the detail is that the agent needs two things, a skills directory and a set of MCP tools. The skills directory is symlinked to the one your coding agent reads, with the paths given for Claude Code, for Codex and for Copilot CLI. The MCP tools are the trace_debugger, spec_analyzer and inv_checking_tool, and the CFA tool has to be built with Maven before the spec_analyzer is added. The trace debugger is installed as a virtual environment with its own requirements, and then registered with the agent, and the registration carries a SPECULA_ROOT environment variable pointing at the checkout so the tool knows where the run data lives.

```bash
# 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
```

```bash
# 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"
```

The README notes that automatic MCP configuration is skipped for older Copilot CLI versions, so you need to upgrade to get it.

## Run modes, and the file that keeps the runs comparable

There are three ways to run Specula and they differ in how much they assume. Auto mode takes a system name, an artifact path pointing at the repository and an optional guidance file, and the guidance is described as a configuration file that guides Specula to focus on target modules and scenarios, with consistent modeling scope across runs, and a template and an example are provided. Outputs are stored in a run identifier directory, and after a run you start with the pipeline summary in the latest run folder. The --keep-original flag is the interesting one, because Specula runs the same agents against a full private copy of the source and writes a reviewable source diff, with ignored build output omitted while binary and trace contents stay in the private copy rather than being inlined, and Specula does not apply the diff to the original checkout. Continuous verification mode is the second command pair, where a persistent model and harness are initialised once and later source changes are checked incrementally against the same CI directory, which the README says should be kept outside the source checkout. Interactive mode is the third, and it is the one to read for the shape of the work, because it opens your coding agent in the Specula directory and runs a sequence of skills where each produces input for the next.

## The interactive sequence tells you how the agent is chained

The interactive workflow is a pipeline of five skills, and the order is the design. The sequence runs code-analysis, then spec-generation, then harness-generation, then validation-workflow, and then bug-confirmation, with the README noting that Codex uses the same names with a dollar sign prefix after choosing an option in the specula command. Reading that sequence tells you how the system is decomposed. Code analysis produces the understanding of the target, which feeds spec generation, which produces the TLA+ specification and the invariants, which feeds harness generation, which produces the executable harness that the model checker drives, which feeds the validation workflow where the properties are checked, which feeds bug confirmation where a violation is turned back into something a developer can look at. Each step is a separate skill, which means each is separately promptable and separately replaceable, and a team that finds one of them weak can substitute their own without rewriting the chain. The README also mentions a hybrid configuration for selecting another agent or model for a particular phase, which is the same idea applied to the model rather than the step.

## The agents you can use, and the access that some of them need

The recommended agents are listed with the models, and the recommendation is backed by testing. The README recommends Claude Code with Claude Opus 4.8 or Fable, and Codex with GPT-5.5 or GPT-5.6-Sol, and says these are the ones actively tested. Other strong coding agents may work but are not tested regularly during development, and the README records that Claude Code with GLM-5.2, Kimi 2.7 and DeepSeek V4 were recently tested, with the details in the usage guide. Then there is a wrinkle worth knowing before you plan a run, because it affects cost and scheduling. For GPT-5.6-Sol and Fable, you apply for Trusted Access through OpenAI and Anthropic respectively, and without the required access, providers may block bug-reproduction requests during confirmation. The fallback is the hybrid configuration, where you select another agent or model for that phase. That is an honest constraint rather than a surprise, since the bug confirmation phase asks the provider to do something that looks like exploiting a vulnerability, and the provider's own safety systems are in the way. The README also asks for adapters to be contributed for new agents, with the adapters living under scripts/launch/adapters.

## Where Specula is the wrong choice

The first limit is that the value depends entirely on the system being concurrent or distributed. A web service that reads a database and returns a response has nothing for a model checker to find, and the hours of agent time and 100 GB of disk would buy nothing. The second is that the specification is still a specification, and an agent that infers an invariant from code can infer the wrong one, in particular an invariant that holds only because the code has a bug, which is the classic way formal verification is made to agree with an implementation rather than to criticise it. The third is the cost and the latency. Running several agents against a copy of a repository, generating models, model checking and reproducing counterexamples is a pipeline that takes a long time, and the continuous verification mode is the answer to that cost, but it is a different kind of project to maintain, since the models become an asset that has to be kept in step with the code. The fourth is the tool maturity, with a version of 1.2.0 and a project that grew from 1.0.0 in August 2026, so the workflow and the CLI will move. And the fifth is that the reproduction step may not be available with the model you have, because provider access policies can block the requests that phase needs, in which case the hybrid configuration is a workaround rather than a fix.

## Conclusion

Adopt Specula if you are verifying concurrent or distributed code and you want a formal model written for you rather than by hand, and you have the machine and the agent budget that implies. Skip it if your system is not concurrent, since that is where its value comes from, or if you need a mature model checking workflow with existing TLA+ assets, since the project is at version 1.2.0 and expects to grow. Verify first that your code has the properties worth stating, since a spec is only as good as the invariants in it, and that your agent provider is one of the tested configurations, since providers may block the bug reproduction requests during confirmation.

## FAQ

### How does Specula find bugs in concurrent system code?

It uses coding agents to write TLA+ specifications of the target system, including invariants capturing its correctness properties and formal models describing the implementation, then model checks the specs and reproduces violations at the code level. The project maintains a list of the bugs it has found and a separate case-study archive with reports, models and reproduction evidence.

### What does Specula need installed before it will run?

Python 3.10 or newer with pip, uv, Java 21 or newer with Maven, the GitHub CLI, and a supported coding agent, with adapters contributed for new ones. The README recommends at least 32 GB of RAM and 100 GB of free disk space, and says Windows users should run it inside WSL2 because native Windows is not supported yet.

### How do I install Specula and run it in auto mode?

Clone the repository, run uv tool install -e . to install the specula command, and run specula setup to install the agent skills and MCP tools and build the bundled tools. Then specula run takes a system name, an artifact path to the repository and an optional guidance file, and outputs are stored in a run identifier directory where the pipeline summary is the place to start reading.

## Sources

- [Issues](https://github.com/specula-org/Specula/issues)
- [License: Apache-2.0](https://github.com/specula-org/Specula/blob/main/LICENSE)
- [README](https://github.com/specula-org/Specula/blob/main/README.md)
- [Releases](https://github.com/specula-org/Specula/releases)
- [specula-org/Specula on GitHub](https://github.com/specula-org/Specula)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/specula-org-specula