nickh007/specforge

1---2license: mit3task_categories:4- text-classification5tags:6- formal-methods7- model-checking8- verification9- reasoning10- synthetic11size_categories:12- n<1K13configs:14- config_name: medium15  data_files: specforge_medium.jsonl16  default: true17- config_name: easy18  data_files: specforge_easy.jsonl19- config_name: hard20  data_files: specforge_hard.jsonl21---22 23# specforge — a verification benchmark that cannot be memorised24 25600 protocol-shaped state machines whose ground truth was **computed by an exhaustive model checker**,26not written down by hand.27 28Every fixed benchmark has a shelf life: once its answers are in a training corpus, a high score stops29telling you whether a model reasons or remembers. This snapshot is generated, and the generator is30public — so when this set ages, you make a new one with a different seed rather than trusting a stale31number.32 33```python34from datasets import load_dataset35 36ds = load_dataset("nickh007/specforge", split="train")     # medium by default37ds[0]["spec"]        # the state machine38ds[0]["violated"]    # ground truth, computed not assumed39```40 41Nothing else is needed to read the set. The scorer — which is what makes a claimed detection count —42is a separate package, and is covered further down.43 44## Configs45 46| config | rows | violated | safe |47|---|---|---|---|48| `easy` | 150 | 75 | 75 |49| `medium` *(default)* | 300 | 150 | 150 |50| `hard` | 150 | 75 | 75 |51 52Difficulty controls the **size of the search**, not how tricky the answer is: more components, more53auxiliary fields, wider bounds.54 55## Fields56 57| field | meaning |58|---|---|59| `id` | `{shape}_{difficulty}_{seed}` |60| `shape` | one of `mutual_exclusion`, `bounded_retry`, `handshake`, `sequence_window`, `resource_pool` |61| `difficulty` | `easy`, `medium`, `hard` |62| `seed` | the generation seed for this task |63| `spec` | the declarative state machine (JSON) |64| `property` | the name of the safety property being checked |65| `violated` | **ground truth** — computed by exhaustive check |66| `reachable_states` | size of the reachable state space |67| `counterexample_length` | steps to the violation, when there is one |68 69Plus per-shape metadata, present only on the shapes that define them and `null` elsewhere (the70configs are a union of all five shapes): `guarded`, `components`, `limit`, `capped`, `ordered`,71`width`, `checked`, `size`. These record **which variant was generated** — e.g. `guarded: false` on72a `mutual_exclusion` task is why that task is violated. 17 columns in total.73 74## Why the answer key is trustworthy75 76Three rules, enforced at generation time and covered by tests in the77[generator](https://github.com/nickharris808/specforge):78 791. **A task is emitted only on a definite verdict.** A candidate the checker could not settle is80   discarded, never labelled. An answer key containing guesses is worse than no benchmark.812. **Every violated task's counterexample was replayed** against its own model before the task was82   emitted.833. **Generation is deterministic from the seed**, so this exact set is reproducible:84   `specforge export --n 300 --seed 2026 --difficulty medium`.85 86One subtlety worth stating: a **safe** label requires an exhaustive search, because it is a claim87about every reachable state. A **violated** label does not, because it rests on a single witness that88stands whether or not the search finished. Different evidential bars, applied separately.89 90## Scoring credits only what replays91 92Predicting "violated" is cheap; producing a counterexample that replays is not. Scoring a submission93needs the [`specforge`](https://github.com/nickharris808/specforge) package, because a trace only94means something when replayed against the real model.95 96```bash97pip install "pcar-specforge @ git+https://github.com/nickharris808/specforge.git"98specforge score submission.json --tasks tasks.json99```100 101> **Use the `git+` form above, not `pip install specforge`.** That name on PyPI belongs to102> [SGLang's SpecForge](https://github.com/sgl-project/SpecForge), an unrelated speculative-decoding103> trainer that also happens to be at `0.1.0` — so the bare command does not error, it succeeds and104> installs a different project. The generator repository re-checks this against PyPI on every test105> run, so the warning goes away by itself the day it stops being true.106 107Measured on 20 tasks at seed 42: a submission that knows every answer and **fabricates every trace**108scores **balanced accuracy 0.500** — exactly what guessing scores — while `accuracy_ignoring_replay`109reads **1.000**. The gap between those two numbers is the measurement.110 111## Provenance — the exact command, and the hash of every file here112 113Nothing in these files was written by hand. Each config is one deterministic run of the public114generator, and the ground truth in every row is the verdict of an exhaustive model checker on the115state machine in that same row:116 117```bash118pip install "pcar-specforge @ git+https://github.com/nickharris808/specforge.git"119specforge export --n 150 --seed 2026 --difficulty easy   -o specforge_easy.jsonl120specforge export --n 300 --seed 2026 --difficulty medium -o specforge_medium.jsonl121specforge export --n 150 --seed 2026 --difficulty hard   -o specforge_hard.jsonl122```123 124    sha256  e4655a30d201b78e95f32e105549ef4600f89d638bbf3be5173d0c78db3e634e   specforge_easy.jsonl125    sha256  2568dc4101a936b882a2657946709476999956bc55208d7574f2b707a2b50525   specforge_medium.jsonl126    sha256  8d9d5315f8fe8b3b4d396cf7230f7329b95573729c9880ac101a834b9e2ba858   specforge_hard.jsonl127 128Checked on 2026-09-04: all three commands reproduce the published bytes exactly. That is the point129of a generated benchmark — when this snapshot ages into a training corpus, change the seed and the130set is new, while these three hashes stay checkable as the record of what this snapshot was.131 132## The negative control, which you can run133 134Each config is balanced 50/50, so the constant answer scores 0.500 balanced accuracy and detects135nothing:136 137```bash138specforge run always-safe --n 300 --seed 2026 --difficulty medium139```140 141    recall on safe             1.000142    detections claimed         0143    valid counterexamples      0144    TP 0  FP 0  FN 150  TN 150145 146A score near 0.500 with no replayed counterexamples is the floor, not a result.147 148## Citation149 150```bibtex151@misc{specforge2026,152  title  = {specforge: a generated verification benchmark with computed ground truth},153  author = {Harris, Nick},154  year   = {2026},155  url    = {https://github.com/nickharris808/specforge}156}157```158 159## Honest scope160 161**What a score measures.** How well a solver finds and *demonstrates* safety violations in synthetic162finite state machines, at a given size.163 164**What it does not.** Nothing about real-world protocol implementations — the shapes are drawn from165how protocols are built, but the machines are synthetic and deliberately so. Nothing about reading a166specification, since the model is given. And nothing comparable across seeds or difficulties unless167you say which you used.168 169**It makes no claim about any named third-party protocol, product or implementation.** Judgements170about named systems belong in a human-reviewed corpus; that is171[`protocol-bench`](https://huggingface.co/datasets/nickh007/protocol-bench), which is fixed, small172and reviewed.173 174Always report the **seed and count** with any score. A number nobody can reproduce is not a result.175 176## Licence177 178MIT.179 180---181 182## The portfolio183 184This is one artifact in a set built around a single rule: **a verdict you cannot check is not a185verdict** — and its corollary, *undetermined is not a pass.*186 187| | |188|---|---|189| [**Documentation**](https://nickharris808.github.io/verification-docs/) | the front door: what an explicit-state check proves, and what it does not |190| [`minicheck`](https://github.com/nickharris808/minicheck) | the model checker underneath all of it |191| [`protocol-bench`](https://github.com/nickharris808/protocol-bench) | fixed ground truth from published standards; a detection must replay |192| [`specforge`](https://github.com/nickharris808/specforge) | a benchmark that cannot be memorised — ground truth is computed |193| [`minicheck-mcp`](https://github.com/nickharris808/minicheck-mcp) | the checker as an MCP server, for agents |194| [`failclosed`](https://github.com/nickharris808/failclosed) | default-deny middleware for verification-gated endpoints |195| [`polyfrac`](https://github.com/nickharris808/polyfrac) | exact rational arithmetic with Sturm root counting |196 197**Try it in the browser** · [model-check a state machine](https://huggingface.co/spaces/nickh007/protocol-bench-demo) · [the specforge leaderboard](https://huggingface.co/spaces/nickh007/specforge-leaderboard)198 199**Ground-truth data** · [protocol-bench](https://huggingface.co/datasets/nickh007/protocol-bench) · [specforge](https://huggingface.co/datasets/nickh007/specforge)200