Paper: Masato Kamba, Hirotake Murakami, Akiyoshi Sannai. Beyond Code Reasoning: A Specification-Anchored Audit Framework for Expert-Augmented Security Verification. arXiv preprint arXiv:2604.26495, 2026.

SPECA is a specification-anchored security audit framework that derives explicit, typed security properties from natural-language specifications and audits implementations through structured proof-attempt reasoning. Where code-driven auditors look for known bug patterns, SPECA invents a property vocabulary from the spec and asks each implementation to prove the invariants — turning specification-level violations into detectable, traceable findings.

📖 Documentation: https://speca.pages.dev/
🧪 Dataset (audit findings): NyxFoundation/vulnerability-reports on HuggingFace
📦 CLI on npm: speca-cli

• Sherlock Ethereum Fusaka Audit Contest (366 submissions, 10 implementations): SPECA recovers all 15 in-scope H/M/L vulnerabilities and discovers 4 novel bugs confirmed by developer fix commits, including a cryptographic invariant violation missed by all 366 contest auditors.
• RepoAudit C/C++ benchmark (15 projects, 35 ground-truth bugs): SPECA matches the best published precision (88.9% with Sonnet 4.5) while surfacing 12 author-validated candidates beyond ground truth — 2 confirmed by upstream maintainers.
• All false positives in deep analysis (N=16) trace to three interpretable root causes mapped to specific pipeline phases — not the usual "the model thought this was a bug" opacity.

# Bootstrap with the TUI (recommended)
npx speca-cli@latest doctor    # check toolchain
npx speca-cli@latest init       # create BUG_BOUNTY_SCOPE.json + TARGET_INFO.json
npx speca-cli@latest run --target 04

# Or run the orchestrator directly
git clone https://github.com/NyxFoundation/speca.git && cd speca
npm install -g @anthropic-ai/claude-code
uv sync && bash scripts/setup_mcp.sh
uv run python3 scripts/run_phase.py --target 04 --workers 4

Outputs land in outputs/<phase>_PARTIAL_*.json. Browse with speca-cli browse outputs/04_PARTIAL_*.json.

Full setup details → Installation · Quickstart (5 min).

All detailed documentation is unified on the documentation site at https://speca.pages.dev/. Source markdown lives under website/docs/. The site is bilingual — Japanese is the default locale; English is selectable via the locale dropdown.

speca/
├── scripts/             # Orchestrator + phase entry points + datasets/ pipeline
├── prompts/             # Per-phase worker prompts
├── benchmarks/          # RQ1 / RQ2 / RQ2b harnesses + paper figures
├── cli/                 # speca-cli (Node + Ink TUI)
├── website/             # Docusaurus documentation source (deployed at speca.pages.dev)
├── tests/               # pytest suite
└── outputs/             # Phase outputs (gitignored)

Issues and pull requests welcome. Please follow the conventions documented in AGENTS.md (if present) and CLAUDE.md. Topic branches off main; CI runs the test suite on every push.

uv run python3 -m pytest tests/ -v --tb=short

For onboarding a new target, you typically only need to write a BUG_BOUNTY_SCOPE.json and TARGET_INFO.json — no code change required. See Bug-bounty scope for the schema.

@misc{kamba2026speca,
  title         = {Beyond Code Reasoning: A Specification-Anchored Audit Framework for Expert-Augmented Security Verification},
  author        = {Kamba, Masato and Murakami, Hirotake and Sannai, Akiyoshi},
  year          = {2026},
  eprint        = {2604.26495},
  archivePrefix = {arXiv},
  primaryClass  = {cs.CR},
  url           = {https://arxiv.org/abs/2604.26495}
}

SPECA is released under the MIT License.

Disclaimer. SPECA is a research artifact. Findings produced by the pipeline are candidate vulnerabilities and must be validated by a human auditor before being reported to a vendor or bug-bounty program. The maintainers make no warranty as to the completeness or correctness of any audit produced by this software.