Skip to content

Specula v1.0.0

Choose a tag to compare

View all tags
@Qian-Cheng-nju Qian-Cheng-nju released this 01 Aug 14:58
v1.0.0
621af1a
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Specula v1.0.0 marks the project's v1 milestone and accompanies the first public arXiv version of the Specula paper. It makes repair loops more precise and recoverable, corrects TLC deadlock-check behavior, and improves Codex usage accounting.

Highlights

  • The paper, Specula: Scaling formal specifications for autonomous model checking of system code, is now publicly available. The README now links directly to the paper and includes a complete BibTeX citation.
  • Repair-loop result handling is now finding-scoped. Phase 3 still performs full trace validation and model checking for affected configurations, but only violations in the current findings.json return to confirmation.
  • Findings retain their evidence across repairs. When a consumed repair removes the original PENDING REPAIR violation, Specula records that artifact as FALSE POSITIVE without another finding-agent run.
  • Repair confirmation now uses a dedicated durable checkpoint tied to the exact committed findings.json. Interrupted runs finish that scoped result pass before returning to upstream phases, and the checkpoint is cleared only after the pass succeeds.
  • The bundled TLC wrapper's -D option now correctly enables deadlock checking.
  • Codex usage accounting now binds to the exact native root session and includes its descendant sessions. It understands current cache-token fields and reports unavailable usage without failing an otherwise successful agent run or guessing between concurrent sessions.

Upgrade notes

After updating an existing checkout, rerun specula setup to refresh the installed skills and tools. Codex plugin users should select plugin again to update specula-codex@specula.

Installation limitations

v1.0.0 remains a source release. Plain wheel and PyPI installation are not supported because the runtime depends on repository-local scripts, skills, and tools. Install from a persistent checkout with uv tool install -e . and keep that checkout in place.

GitHub-generated source archives do not contain submodule contents. Use a recursive Git clone when the curated case-study corpus or submodule-hosted research tools are needed.

Known limitations

  • Native Windows is not supported; use WSL2.
  • Copilot CLI, OpenCode, and Pi do not support Specula's agent-side stop gate.
  • Some frontier models require additional provider access for Phase 4 bug confirmation; use hybrid agent configuration when a different model or provider is needed for that phase.

Full changelog: v0.3.0...v1.0.0

Assets 2
Loading