Specula

Generate formal specifications for your system. Find deep, complex bugs.

Specula uses coding agents to derive TLA+ specifications from real system code, validates them against implementation traces, and model-checks them to uncover violations it can reproduce in code.

Get started Read the Paper View on GitHub
Specula analyzes system code, generates and validates a TLA+ specification, explores its state space, and confirms discovered violations in the implementation.

Autonomous Specifications

Generate TLA+ specifications and correctness properties directly from real system code, continuously refining them throughout the bug-finding process.

Faithful Exploration

Keep the specification aligned with real system behavior while uncovering concurrent behaviors ordinary tests miss.

Reproduced Bugs

Bring each finding back to the implementation and reproduce it as a concrete failure.

Quick start

Get Started in Seconds

Install Specula, configure your coding agent, and point it at a local system repository.

  1. 1
    Install Specula

    Clone the project and install its command-line tool.

  2. 2
    Configure your agent

    Run setup once to install the skills and supporting tools.

  3. 3
    Start a run

    Give Specula a name and the path to your system.

View README quick start
Command
Run this Command: 
git clone https://github.com/specula-org/Specula.git
cd Specula
uv tool install -e .
specula setup

Agent and model support

Supported agents and recommended models

Specula supports multiple coding agents. For best results, use a strong reasoning model at high effort; the models below are recommended based on our testing.

SUPPORTED

Supported Coding Agents

Claude Code
Codex
GitHub Copilot CLI
OpenCode
Pi

RECOMMENDED

Recommended Models

Claude Opus 5
Claude Fable
GPT-5.6-Sol
GPT-5.5
GLM-5.3
GLM-5.2
Kimi K3

Use a strong reasoning model at high effort. Some confirmation workflows require provider-approved access. Learn more

Bug List

Explore bugs found by Specula.

Browse affected systems, bug reports, and reproduction status in the live Specula bug list.

View Bug List
SystemFindingStatus
arc-swapFallback-path use-after-freeFixed
rabbitmq/raLagging node cannot rejoin via snapshotFixed
ScyllaDBRead barrier stalls after voter demotionFixed

Community & support

Questions, bugs, or ideas? Talk to us.

Join the Specula community on Slack to ask questions, share what you are building, and connect with users and contributors. Use GitHub Issues for bug reports and feature requests.
Join our Slack Open a GitHub issue