SPECA: an auditor that starts from the specification, not the source

The property vocabulary is invented, not imported

Most code-driven auditors work from a catalogue: they look for known bug patterns and hope the spec falls out of the code. SPECA inverts that. It derives explicit, typed security properties from a natural-language specification, then audits each implementation by asking it to prove those invariants, reasoning in what the project calls structured proof-attempt form. The consequence is that a finding is a failed proof against a property that came from the document, which is why the README describes the result as turning specification-level violations into detectable, traceable findings. The theory behind it is written up as an arXiv preprint by Masato Kamba, Hirotake Murakami and Akiyoshi Sannai, titled Beyond Code Reasoning: A Specification-Anchored Audit Framework for Expert-Augmented Security Verification, and it is classified as cs.CR.

Phases with gaps in the numbering

The documentation exposes the pipeline as a sequence of phases rather than one opaque run, and the numbering has gaps worth noting: 01a spec discovery, 01b subgraph extraction, 01e property generation, then 02c code resolution, followed by an audit map and a review stage. The missing letters between 01b and 01e, and between 01e and 02c, are what a research codebase looks like when intermediate steps have been folded into neighbours. Each phase has worker prompts under prompts/ and an entry point under scripts/, and every phase writes its own output file. Two concepts recur in the docs as separate pages, proof-attempt and gate review, which tells you a finding is treated as an argument with a review step attached rather than as a bare string in a list.

Numbers measured against other people's work

The headline results are stated in terms of external yardsticks rather than internal demos. In the Sherlock Ethereum Fusaka audit contest, with 366 submissions covering 10 implementations, SPECA recovered all 15 in-scope high, medium and low findings and turned up 4 novel bugs that developer fix commits later confirmed, including a cryptographic invariant violation that all 366 contest auditors missed. On the RepoAudit C and C++ benchmark of 15 projects with 35 ground-truth bugs, it matched the best published precision at 88.9 percent with Sonnet 4.5, while surfacing 12 author-validated candidates beyond the ground truth, two of them confirmed by upstream maintainers. Two details deserve attention. The precision figure is attributed to one model, so it describes that configuration rather than the framework in general. And of the false positives in the deep analysis, all 16 traced to three interpretable root causes mapped to specific pipeline phases, rather than to the usual opacity of a model insisting something was a bug.

Onboarding a target is two JSON files

The cheapest way in is the npm CLI, which starts by checking your toolchain and then writes the two files a run needs:

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

For a new target you usually write just a BUG_BOUNTY_SCOPE.json and TARGET_INFO.json and change no code, which is the point of a scope file existing as a schema. Outputs land in outputs/ with a name carrying the phase, and partial results are named as such, so a run that stops early still leaves something readable; the CLI then browses them with speca-cli browse. Phase outputs are gitignored, so a run does not dirty the working tree. The dataset of audit findings is published separately as NyxFoundation/vulnerability-reports on HuggingFace, which is also the fastest way to see what a completed run looks like.

Two front ends over one vendored Python core

There are two ways to run the pipeline and they share a core. The TUI route is speca-cli, a Node and Ink program you invoke through npx. The direct route clones the repository, installs the Claude Code CLI globally, syncs the Python environment with uv, and runs the setup script before calling the orchestrator:

uv sync && bash scripts/setup_mcp.sh
uv run python3 scripts/run_phase.py --target 04 --workers 4

The worker count is a flag on the phase entry point, so parallelism is a runtime choice rather than a config file. The interesting coupling is in how the CLI gets its Python. A table named core-dependencies in pyproject.toml is declared as the source of truth for cli/scripts/vendor-core.mjs, which generates the vendored core's own pyproject.toml from it, and the comment asks that the version constraints be kept in sync with the root dependency list and with the actual third-party imports under scripts/. So a dependency bump has to land in three places, which is the cost of shipping a Node CLI that runs Python underneath.

The wheel ships one directory

pyproject.toml names the project security-agent at version 0.0.0, requires Python 3.11 or newer, and builds with hatchling. The packaging target is where the intent is clearest: the wheel includes only web/, with scripts/, cli/ and tests/ deliberately left out so the build stays fast and ad-hoc tooling is not published by accident. A console script, speca-web, points at web.server.cli:main, which is the server side of the project. sweagent is not fetched from an index but pinned to a git tag at v1.0.1, and hatchling is told explicitly to allow direct references so that dependency resolves. There is also an opt-in extra called graph-02c holding Tree-sitter and a language pack, added for a deterministic graph-based phase 02c; the comment notes that the ordinary LLM path through that phase needs no extra dependencies, so the grammars are only needed when you pass the graph flag to code resolution.

A research artifact, and it says so

The license is MIT, and immediately after it comes the sentence that should govern how you use any of this: SPECA is a research artifact, findings produced by the pipeline are candidate vulnerabilities, and they must be validated by a human auditor before being reported to a vendor or a bug-bounty program. The maintainers add that they make no warranty as to the completeness or correctness of any audit the software produces. The rest of the project supports that posture rather than contradicting it. The documentation site is bilingual with Japanese as the default locale and English behind a dropdown, the test suite runs under pytest with asyncio_mode set to auto, CI runs it on every push, and topic branches off main. Releases are infrequent and include non-software tags: v0.9.2 on 16 June 2026, v0.9.1 on 8 May, and a benchmark figures tag from the same day. The last push to main is dated 12 August 2026.

Editorial conclusion

SPECA fits a security team that has a written specification to audit against and wants findings that trace to a rule in that document rather than to a pattern someone remembered, and it fits an auditor onboarding a bug-bounty target since a BUG_BOUNTY_SCOPE.json and a TARGET_INFO.json are usually the only files you write. It does not fit anyone treating the output as a report: the project states plainly that findings are candidate vulnerabilities that a human must validate before they go to a vendor or a bounty program, and it disclaims any warranty about completeness or correctness. Before you rely on the headline numbers, note that the benchmark precision of 88.9 percent is attributed to a specific model, Sonnet 4.5, so the figures describe that configuration rather than the framework alone, and check which phase a finding came from, since the false positives it did analyse traced to three named causes rather than to vague model error.

Frequently asked questions

Official sources

1. License: MIT
2. NyxFoundation/speca on GitHub
3. Project website
4. README
5. Releases