# soundnessbench
[](https://github.com/nickharris808/soundnessbench/actions/workflows/ci.yml)
[](data/)
[](#ground-truth)
[](#install)
[](LICENSE)
**A public benchmark for guard-soundness tools — where passing means never certifying a
vulnerability as safe.**
> **Try it now, no install:** [open the live leaderboard](https://huggingface.co/spaces/nickh007/soundnessbench-leaderboard) — every baseline is scored in your browser as the page loads, and you can paste your own answers file without uploading it anywhere.
Ask a security tool "did you find any escapes?" and a clean answer tells you nothing. It is equally
consistent with *the guard is correct* and *you did not look hard enough*. SoundnessBench replaces that
with ground truth: for each task, exactly how many states the guard admits that the safety property
forbids — computed by exhaustive enumeration, sharing no code with any tool being graded.
```bash
pip install "soundnessbench[stack]@git+https://github.com/nickharris808/soundnessbench@main"
```
The `[stack]` extra pulls in `certkit` and `exploit-counter` so the `certkit-stack` entrant can be
graded alongside the reference baselines. Without it everything still runs — the benchmark imports
none of the tools it grades — but the `certkit-stack` row is simply absent from the table below,
because there is nothing installed to grade.
> **Pre-release.** The PyPI name is reserved and publication is imminent; until then the line above
> is the working install. It is tested in CI on Linux, macOS, and Windows.
## 30-second quickstart
```bash
soundnessbench leaderboard
```
```
soundnessbench leaderboard -- 44 tasks
tool gate coverage decisiveness count acc falseC falseA
---------------- ------ -------- ------------- ---------- ------- -------
certkit-stack PASS 100.0% 100.0% 100.0% 0 0
exhaustive PASS 100.0% 100.0% 100.0% 0 0
always-abstain PASS n/a 0.0% n/a 0 0
sampler-1k FAIL 84.1% 100.0% n/a 7 0
always-sound FAIL 47.7% 100.0% n/a 23 0
gate FAIL = the tool certified at least one unsound guard as SOUND.
A failing gate is not redeemable by any other column.
```
That output is a real run, not an illustration.
**Every row in it is a baseline we wrote, scored by an oracle that is also ours.** `certkit-stack`,
`exhaustive`, `always-abstain`, `sampler-1k` and `always-sound` are all in this repository
(`src/soundnessbench/baselines.py`), and the ground truth they are scored against is computed here
by exhaustive enumeration. Nobody else's tool has been run against this suite yet.
That does not make the numbers wrong — they regenerate from the command above, and the two
degenerate strategies fail the gate exactly as they should. It makes them a **demonstration that
the gate bites**, not a ranking of the field, and a reader is entitled to know which of the two
they are looking at before they read the table. The day a tool we did not write is scored here,
this paragraph is what changes.
## The result worth arguing about
**A 1,000-sample random tester scores 84.1% accuracy and still fails.** It false-certifies 7 unsound
guards — it looked, saw nothing, and reported SOUND.
That is not a strawman. It is what testing *does*. The `needle` family contains guards wrong on as
few as **1 state in 262,144**; a thousand random draws miss a gap that rare 99.6% of the time. Any
benchmark whose gaps are all easily sampled cannot tell testing apart from proving, which is the only
distinction here worth measuring.
## Why the headline metric is not accuracy
About 48% of tasks are sound. So `always-sound` — a tool that answers SOUND to everything and does no
work at all — scores 47.7% and looks like it is doing something. It also certifies all 23
vulnerabilities in the suite as safe.
In security the two error directions are not comparable:
| Error | Cost |
|---|---|
| **False certification** — SOUND on an unsound guard | ships a vulnerability. Unbounded. |
| **False alarm** — UNSOUND on a sound guard | wastes an afternoon. Bounded. |
| **Abstention** — "I cannot decide" | honest, and useful if not universal. |
So the gate is **false certifications must be zero**, and no other column can redeem a failure. Then:
- **coverage** — accuracy over what it answered
- **decisiveness** — how much it was willing to answer
- **count accuracy** — of the exact counts offered, how many were right
Neither degenerate strategy wins. Answer everything and you risk a false certification. Abstain on
everything and coverage is undefined while decisiveness is zero. `always-abstain` passes the gate and
is obviously useless — which is the point of publishing it.
## Submitting
```bash
soundnessbench tasks --out tasks.json # answers stripped
# ... run your tool, emit [{"task_id": ..., "verdict": "SOUND"|"UNSOUND"|"ABSTAIN"}, ...]
soundnessbench submit --answers answers.json --tool my-tool
```
`submit` **validates before it scores**, and stops on anything that would make the number
misleading rather than merely low:
```
error: unknown task id 'nope-1'. It will be ignored, so this answer earns nothing.
Run 'soundnessbench tasks' for the current ids.
error: duplicate answers for bounds-000. Only the last is scored, so the others are
silently discarded -- submit one answer per task.
note: 43 task(s) have no answer and are scored as abstentions: bounds-001, ... .
Abstaining is allowed and never fails the gate; it lowers decisiveness only.
2 problem(s) must be fixed before this submission is meaningful. Nothing was scored.
```
A typo'd task id used to become a silent abstention, so you saw a low score and no reason for it.
Missing answers stay a *warning*, because abstaining is legitimate.
On success it prints your row in exactly the format the leaderboard uses:
```
Your row, as it would appear on the leaderboard:
tool gate coverage decisiveness count acc falseC falseA
---------------- ------ -------- ------------- ---------- ------- -------
my-tool PASS 100.0% 100.0% 100.0% 0 0
```
Use `soundnessbench score` instead if you want scoring with no validation.
Exit code is `0` if you pass the soundness gate and `1` if you false-certify anything, so this works
as a CI gate on your own tool. (`submit` exits `2` when validation stops the run.)
Optionally include `"over_acceptance": ` to be scored on exact counts too. Getting the count
wrong does not change your verdict score — a tool that correctly says UNSOUND without quantifying is
still useful.
**Omitted answers count as abstentions**, so you cannot raise coverage by dropping the hard tasks.
## The hard split: real CVE relations
The task families below are synthetic, and `SCOPE.md` has always said so. That is the strongest
objection to the benchmark — seven generated shapes can be tuned for. The **hard split** answers it.
```bash
soundnessbench --split hard leaderboard
soundnessbench --split hard tasks --out tasks.json
```
Every relation in it comes from the published
[cve-proof-corpus](https://huggingface.co/datasets/nickh007/cve-proof-corpus): the check a real
historical vulnerability class turned on, transcribed as linear atoms. Real specs bring more
variables, more domain constraints, and several safety conjuncts, so a tool that handles one guard
atom over two variables can score well on the public split and fall over here.
**The unsound variants are constructed, and the construction is the interesting part.** The first
design used fixed weakenings — relax by one, relax by eight — and it did not work: on relations with
slack between the guard and the safety property, those edits changed nothing, so most tasks came out
sound and "always answer SOUND" scored about three quarters of them. A benchmark a constant answer
beats is not measuring anything. (That design was discarded, so those figures cannot be reproduced
from this code — they are recorded as the reason for the current design, not as a result.)
So the split asks a sharper question: **what is the smallest edit that breaks this guard?** For each
relation, an exhaustive search finds the minimal relaxation `k` that admits a forbidden state. The
split then contains the guard relaxed by `k` (unsound by exactly one step) and, where `k > 1`, by
`k − 1` (sound by exactly one step). Getting the order of magnitude right is not enough.
| Family | What it is |
|---|---|
| `cve-fixed` | The relation as fixed, unmodified. Sound. |
| `cve-edge-unsound` | Relaxed by the minimal breaking edit. Unsound by one step. |
| `cve-edge-sound` | Relaxed by one less than that. Sound by one step. |
| `cve-dropped` | A guard conjunct removed entirely, as a refactor might. |
Nothing here is a statement about any current version of any software. The relations are historical
and public; the weakenings are constructed, are not code any project shipped, and every task says so
in its note.
Boxes are narrowed where a real variable's range is too wide to enumerate — and the task records the
narrowing and the real bound, because narrowing changes the question. The rule the public split
follows applies unchanged: **every answer comes from exhaustive enumeration**, or it does not ship.
**Score in your browser:** [the leaderboard
Space](https://huggingface.co/spaces/nickh007/soundnessbench-leaderboard) runs the whole benchmark
client-side. Your submission is never uploaded.
## Task families
| Family | Shape | The trap |
|---|---|---|
| `bounds` | `off + len <= cap` | guard permits extra states (CWE-787 / CWE-125) |
| `heartbleed` | `overhead + payload <= record_len` | overhead too small (CVE-2014-0160) |
| `index` | `scale*i < n` | `<=` where `<` was required (CWE-129) |
| `offbyone` | `x <= cap-1` | the classic bound-by-one |
| `twovar` | two coupled constraints | both conjuncts must hold |
| `wrap` | per-operand bounds | do they compose to a sum bound? |
| `needle` | rare gap | **1–6 violating states in up to 262,144** |
## Ground truth
Answers are precomputed and committed to `data/ground_truth.json`, because brute-forcing all 44
tasks costs ~3 seconds and was being paid on **every** CLI invocation — `soundnessbench tasks` spent
3 seconds computing answers it then stripped from its own output. It now takes about 60 ms, most of which is Python starting up — time it yourself with `time soundnessbench tasks --out /tmp/t.json`.
The obvious risk is a stale file. Two things prevent it:
- **Entries are keyed by a content hash of each task's relations**, not by task id. Change a
relation and the key changes, the lookup misses, and the answer is recomputed. A stale entry is
unreachable, not merely detectable.
- **`soundnessbench verify-ground-truth`** recomputes everything by enumeration and compares. Run it
in CI. `--write` regenerates after an intended change.
```bash
$ soundnessbench verify-ground-truth
44 of 44 answers match a fresh enumeration.
The precomputed ground truth is a cache, not a claim.
```
The file is a cache in the strict sense: deleting it changes speed, never answers.
## How the answers are computed
Every answer comes from point-by-point enumeration of the declared box — the dumbest available
algorithm, chosen because it is too simple to be wrong in an interesting way. `soundnessbench` does not
import `certkit`, because it has to be able to grade `certkit`.
The test suite re-derives all 44 answers a second, independently written way, and verifies that every
stored witness genuinely satisfies the guard while violating safety.
## Limitations
- **Quantifier-free linear integer arithmetic only.** No nonlinear terms, no heap, no aliasing, no
floats. Doing well here does not make a tool a program verifier.
- **Small boxes by construction.** Ground truth must be enumerable, so the largest box is 262,144
points. A tool that scales to 2^32 gets no credit for it here.
- **Synthetic instances with real shapes.** Modelled on real vulnerability classes; not extracted
from production code.
- **44 tasks is small.** Family-level breakdowns are indicative, not statistically strong.
- **Over-acceptance is triggerability, not severity.** Not CVSS, not a weaponisability claim.
## Dataset
The suite is published as JSONL with a dataset card in [`data/`](data/), suitable for a dataset hub.
Both splits ship: one with ground truth, one with the answer key stripped.
```bash
soundnessbench dataset --out soundnessbench-v1.jsonl --with-answers
```
Generation is deterministic — same seed, byte-identical tasks — so a published score reproduces.
## Tests
```bash
pip install -e ".[dev]"
pytest
```
143 tests. The load-bearing ones are `test_always_sound_fails_the_gate` (the metric is not gameable)
and `test_sampler_false_certifies_the_rare_gaps` (the needles are genuinely rare). If the second ever
stops failing the sampler, the benchmark has lost its reason to exist.
## Documentation
| | |
|---|---|
| [`SCOPE.md`](SCOPE.md) | what a passing gate does and does not establish |
| [certkit's TUTORIAL](https://github.com/nickharris808/certkit/blob/main/TUTORIAL.md) | end-to-end worked example |
## The rest of the toolkit
| | |
|---|---|
| **[certkit](https://github.com/nickharris808/certkit)** | the certificate format and the independent checker |
| **[exploit-counter](https://github.com/nickharris808/exploit-counter)** | if a guard is unsound, exactly how many states escape |
| **[crs-mcp](https://github.com/nickharris808/crs-mcp)** | the verdict surface AI coding agents call, over MCP |
| **[soundnessbench](https://github.com/nickharris808/soundnessbench)** | the benchmark that grades all of the above |
| **[certkit-action](https://github.com/nickharris808/certkit-action)** | run the check in your CI |
| **[pytest-mutation-verified](https://github.com/nickharris808/pytest-mutation-verified)** | prove your regression test can actually fail |
| **[cve-proof-corpus](https://huggingface.co/datasets/nickh007/cve-proof-corpus)** | six real CVEs with machine-checkable proofs |
| **[Try it in your browser](https://huggingface.co/spaces/nickh007/certkit-demo)** | no install; watch a forgery get refused |
---
## The closed core
These packages are the *checking* half. They deliberately contain no proof search, which is what keeps
them small enough to audit — and it means something upstream has to produce certificates.
For obligations over full machine-word domains, enumeration does not scale and a decision procedure
that does not enumerate is required: solver-free elimination emitting replayable certificates. That
engine, the repair synthesiser that derives a minimal guard from a refutation, and the evolutionary
search that drives them are **not** in this repository and are available commercially.
The split is deliberate and permanent. **The checker is free and always will be** — a certificate you
cannot independently verify is worth nothing, so charging for verification would defeat the format.
What costs money is *producing* certificates at scale.
## License
Apache-2.0. The benchmark and its data are meant to be copied, forked, and argued with.
## Licence, citation, contributing
Apache-2.0 ([`LICENSE`](LICENSE)). If you use this in work you publish, there is machine-readable
citation metadata in [`CITATION.cff`](CITATION.cff) — GitHub's "Cite this repository" button reads it.
- [`CONTRIBUTING.md`](CONTRIBUTING.md) — the house rules, and the one invariant a change must not break.
- [`ARCHITECTURE.md`](ARCHITECTURE.md) — the module map and where the trust boundary sits.
- [`TROUBLESHOOTING.md`](TROUBLESHOOTING.md) — keyed to the error messages this actually prints.
- [`SECURITY.md`](SECURITY.md) — a checker that accepts something false is the highest severity class here.
---
Part of **[certified discovery](https://nickharris808.github.io/certified-discovery/)** — ten artifacts built on one asymmetry: checking a proof is cheap and auditable, so the thing that produced it does not have to be trusted.