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

Default setup. The same installation works with every supported coding agent.

Broad agent support

Use the coding agents you already trust.

One workflow across supported agent CLIs, with actively tested model recommendations.

SUPPORTED

Coding Agents

CCClaude Code
OXCodex
GHCopilot CLI
OCOpenCode
PIPi

ACTIVELY TESTED

Recommended Models

ClaudeOpus 4.8
ClaudeFable
CodexGPT-5.5
CodexGPT-5.6-Sol

Some confirmation workflows require provider-approved access. Learn more

Bug List

A searchable catalog is coming soon.

We are preparing a structured view of bugs found by Specula, including affected systems, evidence, and reproduction status.

View the current list
Coming soon

Research

Cite Specula

If Specula is useful in your research, please cite the paper.

Read the paper
BibTeX 
@misc{cheng2026specula,
  title         = {{Specula}: Scaling formal specifications for autonomous
                   model checking of system code},
  author        = {Qian Cheng and Saad Mohammad Rafid Pial and Ruize Tang and
                   Yiming Su and Emilie Ma and Finn Hackett and
                   Ivan Beschastnikh and Yu Huang and Tianyin Xu},
  year          = {2026},
  eprint        = {2607.25333},
  archivePrefix = {arXiv},
  primaryClass  = {cs.SE},
  url           = {https://arxiv.org/abs/2607.25333}
}

Community & support

Questions, bugs, or ideas? Talk to us.

Open an issue to ask for help, report a problem, or suggest where Specula should go next.
Contact us on GitHub