Summary

SPECA is a specification-anchored security auditing framework that derives explicit, typed security properties from natural-language specifications. It targets security auditors and developers, enabling them to audit code implementations by proving derived invariants. This approach transforms specification-level violations into traceable findings, discovers novel bugs missed by traditional methods, and offers interpretable root causes for potential issues.

How It Works

SPECA employs a novel specification-anchored approach, deriving explicit, typed security properties from natural-language specifications. It then audits code implementations by generating structured proof attempts to verify these invariants. This method deviates from pattern-matching auditors by inventing a property vocabulary directly from the specification, allowing it to detect violations at a deeper, conceptual level and uncover previously unknown vulnerabilities.

Quick Start & Requirements

Recommended setup uses the CLI: npx speca-cli@latest doctor and npx speca-cli@latest init. Alternatively, clone the repo, install global Node.js (@anthropic-ai/claude-code) and Python (uv sync) dependencies, set up the model pipeline (bash scripts/setup_mcp.sh), and run the orchestrator (uv run python3 scripts/run_phase.py). Prerequisites include Node.js, Python 3, and potentially an Anthropic API key. Setup is estimated at 5 minutes. Documentation: https://speca.pages.dev/.

Highlighted Details

• In the Sherlock Ethereum Fusaka Audit Contest (366 submissions), SPECA identified all 15 in-scope vulnerabilities and discovered 4 novel bugs, including a cryptographic invariant violation missed by all other auditors.
• On the RepoAudit C/C++ benchmark, SPECA achieved 88.9% precision (matching best published results) and surfaced 12 additional author-validated candidates.
• False positives revealed interpretable root causes tied to specific pipeline phases, offering transparency beyond typical model opacity.

Maintenance & Community

The repository structure indicates active development. However, the README does not detail specific contributors, community channels (like Discord or Slack), sponsorships, or a public roadmap.

Licensing & Compatibility

SPECA is released under the permissive MIT License, generally allowing for commercial use and integration into closed-source projects without significant restrictions.

Limitations & Caveats

SPECA is presented as a research artifact. All findings are candidate vulnerabilities requiring human validation before external reporting. Maintainers disclaim any warranty regarding the completeness or correctness of the audits produced.