nickh007/specforge

specforge — a verification benchmark that cannot be memorised

600 protocol-shaped state machines whose ground truth was computed by an exhaustive model checker, not written down by hand.

Every fixed benchmark has a shelf life: once its answers are in a training corpus, a high score stops telling you whether a model reasons or remembers. This snapshot is generated, and the generator is public — so when this set ages, you make a new one with a different seed rather than trusting a stale number.

from datasets import load_dataset

ds = load_dataset("nickh007/specforge", split="train")     # medium by default
ds[0]["spec"]        # the state machine
ds[0]["violated"]    # ground truth, computed not assumed

Nothing else is needed to read the set. The scorer — which is what makes a claimed detection count — is a separate package, and is covered further down.

Configs

Difficulty controls the size of the search, not how tricky the answer is: more components, more auxiliary fields, wider bounds.

Fields

Plus per-shape metadata, present only on the shapes that define them and null elsewhere (the configs are a union of all five shapes): guarded, components, limit, capped, ordered, width, checked, size. These record which variant was generated — e.g. guarded: false on a mutual_exclusion task is why that task is violated. 17 columns in total.

Why the answer key is trustworthy

Three rules, enforced at generation time and covered by tests in the generator:

1. 1.A task is emitted only on a definite verdict. A candidate the checker could not settle is discarded, never labelled. An answer key containing guesses is worse than no benchmark.
2. 2.Every violated task's counterexample was replayed against its own model before the task was emitted.
3. 3.Generation is deterministic from the seed, so this exact set is reproducible: specforge export --n 300 --seed 2026 --difficulty medium.

One subtlety worth stating: a safe label requires an exhaustive search, because it is a claim about every reachable state. A violated label does not, because it rests on a single witness that stands whether or not the search finished. Different evidential bars, applied separately.

Scoring credits only what replays

Predicting "violated" is cheap; producing a counterexample that replays is not. Scoring a submission needs the `specforge` package, because a trace only means something when replayed against the real model.

pip install "pcar-specforge @ git+https://github.com/nickharris808/specforge.git"
specforge score submission.json --tasks tasks.json

Use the `git+` form above, not `pip install specforge`. That name on PyPI belongs to SGLang's SpecForge, an unrelated speculative-decoding trainer that also happens to be at 0.1.0 — so the bare command does not error, it succeeds and installs a different project. The generator repository re-checks this against PyPI on every test run, so the warning goes away by itself the day it stops being true.

Measured on 20 tasks at seed 42: a submission that knows every answer and fabricates every trace scores balanced accuracy 0.500 — exactly what guessing scores — while accuracy_ignoring_replay reads 1.000. The gap between those two numbers is the measurement.

Provenance — the exact command, and the hash of every file here

Nothing in these files was written by hand. Each config is one deterministic run of the public generator, and the ground truth in every row is the verdict of an exhaustive model checker on the state machine in that same row:

pip install "pcar-specforge @ git+https://github.com/nickharris808/specforge.git"
specforge export --n 150 --seed 2026 --difficulty easy   -o specforge_easy.jsonl
specforge export --n 300 --seed 2026 --difficulty medium -o specforge_medium.jsonl
specforge export --n 150 --seed 2026 --difficulty hard   -o specforge_hard.jsonl

sha256 e4655a30d201b78e95f32e105549ef4600f89d638bbf3be5173d0c78db3e634e specforgeeasy.jsonl sha256 2568dc4101a936b882a2657946709476999956bc55208d7574f2b707a2b50525 specforgemedium.jsonl sha256 8d9d5315f8fe8b3b4d396cf7230f7329b95573729c9880ac101a834b9e2ba858 specforge_hard.jsonl

Checked on 2026-09-04: all three commands reproduce the published bytes exactly. That is the point of a generated benchmark — when this snapshot ages into a training corpus, change the seed and the set is new, while these three hashes stay checkable as the record of what this snapshot was.

The negative control, which you can run

Each config is balanced 50/50, so the constant answer scores 0.500 balanced accuracy and detects nothing:

specforge run always-safe --n 300 --seed 2026 --difficulty medium

recall on safe 1.000 detections claimed 0 valid counterexamples 0 TP 0 FP 0 FN 150 TN 150

A score near 0.500 with no replayed counterexamples is the floor, not a result.

Citation

@misc{specforge2026,
  title  = {specforge: a generated verification benchmark with computed ground truth},
  author = {Harris, Nick},
  year   = {2026},
  url    = {https://github.com/nickharris808/specforge}
}

Honest scope

What a score measures. How well a solver finds and demonstrates safety violations in synthetic finite state machines, at a given size.

What it does not. Nothing about real-world protocol implementations — the shapes are drawn from how protocols are built, but the machines are synthetic and deliberately so. Nothing about reading a specification, since the model is given. And nothing comparable across seeds or difficulties unless you say which you used.

It makes no claim about any named third-party protocol, product or implementation. Judgements about named systems belong in a human-reviewed corpus; that is `protocol-bench`, which is fixed, small and reviewed.

Always report the seed and count with any score. A number nobody can reproduce is not a result.

Licence

MIT.

The portfolio

This is one artifact in a set built around a single rule: a verdict you cannot check is not a verdict — and its corollary, undetermined is not a pass.

Try it in the browser · model-check a state machine · the specforge leaderboard

Ground-truth data · protocol-bench · specforge