---
license: mit
task_categories:
- text-classification
tags:
- formal-methods
- model-checking
- verification
- reasoning
- synthetic
size_categories:
- n<1K
configs:
- config_name: medium
  data_files: specforge_medium.jsonl
  default: true
- config_name: easy
  data_files: specforge_easy.jsonl
- config_name: hard
  data_files: specforge_hard.jsonl
---

# 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.

```python
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

| config | rows | violated | safe |
|---|---|---|---|
| `easy` | 150 | 75 | 75 |
| `medium` *(default)* | 300 | 150 | 150 |
| `hard` | 150 | 75 | 75 |

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

## Fields

| field | meaning |
|---|---|
| `id` | `{shape}_{difficulty}_{seed}` |
| `shape` | one of `mutual_exclusion`, `bounded_retry`, `handshake`, `sequence_window`, `resource_pool` |
| `difficulty` | `easy`, `medium`, `hard` |
| `seed` | the generation seed for this task |
| `spec` | the declarative state machine (JSON) |
| `property` | the name of the safety property being checked |
| `violated` | **ground truth** — computed by exhaustive check |
| `reachable_states` | size of the reachable state space |
| `counterexample_length` | steps to the violation, when there is one |

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](https://github.com/nickharris808/specforge):

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. **Every violated task's counterexample was replayed** against its own model before the task was
   emitted.
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`](https://github.com/nickharris808/specforge) package, because a trace only
means something when replayed against the real model.

```bash
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](https://github.com/sgl-project/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:

```bash
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   specforge_easy.jsonl
    sha256  2568dc4101a936b882a2657946709476999956bc55208d7574f2b707a2b50525   specforge_medium.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:

```bash
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

```bibtex
@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`](https://huggingface.co/datasets/nickh007/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.*

| | |
|---|---|
| [**Documentation**](https://nickharris808.github.io/verification-docs/) | the front door: what an explicit-state check proves, and what it does not |
| [`minicheck`](https://github.com/nickharris808/minicheck) | the model checker underneath all of it |
| [`protocol-bench`](https://github.com/nickharris808/protocol-bench) | fixed ground truth from published standards; a detection must replay |
| [`specforge`](https://github.com/nickharris808/specforge) | a benchmark that cannot be memorised — ground truth is computed |
| [`minicheck-mcp`](https://github.com/nickharris808/minicheck-mcp) | the checker as an MCP server, for agents |
| [`failclosed`](https://github.com/nickharris808/failclosed) | default-deny middleware for verification-gated endpoints |
| [`polyfrac`](https://github.com/nickharris808/polyfrac) | exact rational arithmetic with Sturm root counting |

**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)

**Ground-truth data** · [protocol-bench](https://huggingface.co/datasets/nickh007/protocol-bench) · [specforge](https://huggingface.co/datasets/nickh007/specforge)