> **Distribution name (2026-08-18): `pcar-specforge`.** The repository is `specforge`; the
> PyPI distribution cannot be, because that name is owned by the SGLang project. `pip install pcar-specforge` does not work yet — the name is registered to nobody and this project has not been uploaded. Install with the `git+` form below.

# specforge

[![install](https://img.shields.io/badge/install-git%2Bhttps-blue)](https://github.com/nickharris808/specforge#install)
[![CI](https://github.com/nickharris808/specforge/actions/workflows/ci.yml/badge.svg)](https://github.com/nickharris808/specforge/actions/workflows/ci.yml)
[![tests](https://img.shields.io/badge/tests-82%20passing-brightgreen)](tests/)
[![python](https://img.shields.io/badge/python-3.9%2B-blue)](pyproject.toml)
[![license](https://img.shields.io/badge/license-MIT-green)](LICENSE)

**A verification benchmark that cannot be memorised. Ground truth is computed, not written down.**

## Why this exists

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 — and nothing in the score tells you which one you
are looking at.

`specforge` generates the tasks instead. Each one is a synthetic state machine built from the shapes
protocols are made of, and its answer comes from running an exhaustive model checker on it rather
than from a label a human wrote. Change the seed and you get a fresh set that nothing has seen.

## Install

```
pip install "pcar-specforge @ git+https://github.com/nickharris808/specforge.git"
```

That pulls in [`minicheck`](https://github.com/nickharris808/minicheck) automatically. Python 3.9+,
no other dependencies.

> ### ⚠ Do not run `pip install specforge`
>
> **The bare name `specforge` on PyPI is owned by the SGLang project** —
> [SGLang's SpecForge](https://github.com/sgl-project/SpecForge), an unrelated speculative-decoding
> training framework, at version `0.2.0`. So that command does not error —
> it succeeds and installs a completely different project.
>
> This project's distribution name is **`pcar-specforge`**, which is not on PyPI at all.
>
> ```console
> $ curl -s -o /dev/null -w '%{http_code}\n' https://pypi.org/pypi/specforge/json
> 200
> $ curl -s https://pypi.org/pypi/specforge/json | python3 -c "import json,sys; d=json.load(sys.stdin)['info']; print(d['name'], d['version'], '|', d['author'], '|', d['home_page'])"
> specforge 0.2.0 | SGLang Team | None
> ```
>
> ```console
> $ curl -s -o /dev/null -w '%{http_code}\n' https://pypi.org/pypi/pcar-specforge/json
> 404
> ```
>
> Always use the `git+` form above, which is unambiguous. The rename to `pcar-specforge` is what
> makes an index release possible at all; claiming that name on PyPI is a human decision that has
> not been taken. `python build_pypi.py` produces an uploadable artifact.
>
> `tests/test_install_line.py` re-checks the name against PyPI on every run, so this warning
> disappears the day it stops being true — and would appear on any other package the day one of
> those names is taken.

## 30-second quickstart

Real output from `specforge run bfs --n 20 --seed 42`, verbatim:

```console
$ specforge run bfs --n 20 --seed 42
baseline: bfs
  tasks                      20
  balanced accuracy          1.000   <- headline
  accuracy                   1.000
  (trivial always-safe acc.  0.500)
  recall on violated         1.000
  recall on safe             1.000
  detections claimed         10
  valid counterexamples      10
  unreplayed claims          0
  TP 10  FP 0  FN 0  TN 10
$ echo $?
0
```

```python
from specforge import bfs_baseline, generate, score

tasks = generate(20, seed=42)          # deterministic: same seed, same tasks
res = score(bfs_baseline(tasks), tasks)
res["balanced_accuracy"]               # 1.0
```

## What makes the answer key trustworthy

Three rules, each enforced at generation time and each covered by a test:

1. **A task is emitted only on a definite verdict.** If the checker cannot settle a candidate, the
   candidate is discarded — never labelled. An answer key containing guesses is worse than no
   benchmark, because it looks authoritative.
2. **Every violated task ships a counterexample that replays**, re-verified against its own model
   before the task is emitted. A witness that does not replay is not a witness.
3. **Generation is deterministic from the seed**, so any score anyone reports is reproducible by
   anyone else.

There is one subtlety worth stating, because it is the discipline the whole portfolio rests on. A
task labelled **safe** requires an *exhaustive* search — it is a claim about every reachable state. A
task labelled **violated** does not, because it rests on a single witness that stands whether or not
the search finished. Those are different evidential bars and the generator applies them separately.

## Scoring credits only what replays

Predicting "violated" is cheap. Producing a counterexample that replays is not.

| submission on a violated task | scored as |
|---|---|
| `violated` + a trace that replays | true positive |
| `violated` + a fabricated trace | false negative |
| `violated` + no trace | false negative |
| not `violated` | false negative |

On a safe task, any violation claim is a false positive.

Measured on `--n 20 --seed 42`:

| submission | balanced accuracy | true positives |
|---|---|---|
| `bfs` (runs the checker, real traces) | **1.000** | 10 |
| `always-safe` (guesses) | 0.500 | 0 |
| **knows every answer, fabricates every trace** | **0.500** | **0** |

That last row is the point. A submission with a perfect answer key and no evidence scores exactly
what guessing scores. `accuracy_ignoring_replay` is reported alongside — for that submission it is
**1.000**, and the gap between the two numbers is the measurement.

## Task shapes

Five structural families, named for what they resemble:

| shape | what it models | how it can fail |
|---|---|---|
| `mutual_exclusion` | processes contending for a lock | the lock guard is dropped |
| `bounded_retry` | a retry counter | nothing stops it before the limit |
| `handshake` | request → response → install | a reply is accepted out of order |
| `sequence_window` | a sliding sequence number | it wraps past the window |
| `resource_pool` | acquire/release against a pool | acquisition is unguarded |

Three difficulties (`easy`, `medium`, `hard`) control the **size of the search**, not how tricky the
answer is — more components, more auxiliary fields, wider bounds.

## CLI reference

| Command | What it does |
|---|---|
| `specforge generate --n N --seed S -o tasks.json` | write a task set with its answer key |
| `specforge export --n N --seed S -o tasks.jsonl` | one self-contained JSON object per line |
| `specforge run {bfs,always-safe}` | run a built-in baseline and score it |
| `specforge score sub.json --tasks tasks.json` | score a submission |
| `specforge info` | the shapes and difficulty settings |

Common flags: `--n N` (task count), `--seed S`, `--difficulty {easy,medium,hard}`, `-o FILE`,
`--json` for machine-readable output.

Exit codes: `0` met the threshold, `1` did not, `3` misconfigured. A missing file is **3**, never a
silent pass on nothing.

`specforge info` prints the generator's actual settings, so the difficulty knobs are never a guess:

```console
$ specforge info
shapes:       mutual_exclusion, bounded_retry, handshake, sequence_window, resource_pool
difficulties: easy, medium, hard
  easy     components=2 extra_fields=0 bound=4
  medium   components=3 extra_fields=1 bound=6
  hard     components=4 extra_fields=2 bound=8
```

## Python API reference

| Name | What it does |
|---|---|
| `generate(n, seed=..., difficulty=...)` | a deterministic list of `Task`, each with a settled label |
| `generate_one(...)` | one task, or **`None`** if the checker could not settle it — never a guess |
| `Task.build()` | the `minicheck.Protocol` for that task |
| `Task.property` | the name of the safety property being checked |
| `Task.is_violated` | ground truth, computed by exhaustive search |
| `Task.counterexample` / `Task.counterexample_length` | the shipped replaying witness, when violated |
| `Task.as_dict()` | a self-contained JSON-safe row |
| `score(submission, tasks)` | the full report (keys below) |
| `validate_trace(task, trace)` | replay one claimed counterexample; returns `{valid, reason}` |
| `bfs_baseline(tasks)` / `always_safe_baseline(tasks)` | the two reference submissions |
| `summarise(result)` | the text block the CLI prints |
| `SHAPES` / `DIFFICULTIES` | the generator's shape names and difficulty settings |

`Task` fields: `id`, `shape`, `difficulty`, `seed`, `spec`, `property`, `is_violated`,
`reachable_states`, `counterexample`, `counterexample_length`, `meta`.

### What `score()` returns

| Key | Meaning |
|---|---|
| `balanced_accuracy` | **headline.** Mean of per-class recall, computed from *credited* detections |
| `accuracy` | plain accuracy, also replay-gated |
| `accuracy_ignoring_replay` | what the score would be if claims were taken at face value |
| `unreplayed_claims` | detections claimed whose trace did not replay |
| `valid_counterexamples` | detections whose trace did replay |
| `true_positives` / `false_positives` / `false_negatives` / `true_negatives` | the confusion matrix |
| `trivial_always_safe_accuracy` | what guessing "safe" everywhere scores on this set |
| `by_shape` | the same breakdown per structural family |
| `per_task` | one row per task: `predicted_violated`, `credited_detection`, `outcome`, `trace`, `shape`, `difficulty` |
| `n_tasks` | how many tasks were scored |

The gap between `accuracy_ignoring_replay` and `accuracy` is the measurement: it is how much a
submission asserted beyond what it demonstrated.

## Worked example — evaluate your own solver

```python
from specforge import generate, score, validate_trace

tasks = generate(50, seed=2026, difficulty="hard")

submission = {}
for task in tasks:
    model = task.build()                    # a minicheck.Protocol
    verdict, trace = my_analyser(model, task.property)
    submission[task.id] = {"violated": verdict, "trace": trace}

res = score(submission, tasks)
print(res["balanced_accuracy"], res["unreplayed_claims"])

# Why a specific claim was not credited:
for row in res["per_task"]:
    if row["predicted_violated"] and not row["credited_detection"]:
        print(row["id"], row["trace"]["reason"])
```

Report the **seed and count** alongside any score. Without them the number is not reproducible, and
a number nobody can reproduce is not a result.

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

- Nothing about real-world protocol implementations. The shapes are drawn from how protocols are
  built; the machines are synthetic and deliberately so.
- Nothing about specification reading. The model is given; inferring one from prose is a harder and
  different problem.
- Nothing comparable across seeds or difficulties without saying which you used.

**What it deliberately does not do.** It makes no claim about any named third-party protocol,
product or implementation. Judgements about named systems belong in a corpus a human has reviewed —
not in one a generator emits. If you want ground-truth tasks drawn from published standards, that is
[`protocol-bench`](https://github.com/nickharris808/protocol-bench), which is fixed, small, and
reviewed.

**`bfs` is the ceiling, not a competitor.** It is sound and complete over a model already formalised
for it. The open problem is doing this from a description.

## Performance

Measured on an M-series laptop, CPython 3.11 — reproduce with
`python -c "import time; from specforge import generate; t=time.perf_counter(); generate(20, seed=42); print(time.perf_counter()-t)"`:

| call | wall time |
|---|---|
| `generate(20, seed=42)` (medium) | ~3 ms |
| `generate(20, seed=5, difficulty="hard")` | ~5 ms |

Cost scales with the **state space**, not the task count, because each task runs a full exhaustive
check before it is labelled. Measured `reachable_states` over 20 tasks at seed 42: `easy` 3–129
(mean 18), `medium` 8–256 (mean 40), `hard` 16–508 (mean 95). Nothing here has needed optimising.

## Troubleshooting

**`pip install specforge` installed something about speculative decoding.** It did. That name on
PyPI is [SGLang's SpecForge](https://github.com/sgl-project/SpecForge), an unrelated project. Use
the `git+` URL in [Install](#install).

**My submission scored 0 true positives but I got the verdicts right.** A detection is credited only
when its trace replays. Read `unreplayed_claims`, then the per-task `trace["reason"]`.

**`reason: "a step does not name the fields (...)"`.** Each trace entry is
`{"state": {field: value, ...}}` with **every** field present, including the generated `aux*` fields.
Get the field list from `task.build().fields`.

**`generate_one` returned `None`.** That is the design, not a failure: the checker could not settle
that candidate, so it is discarded rather than labelled. `generate(n, ...)` retries until it has `n`
settled tasks.

**My score does not match someone else's.** Tasks are generated. A score means nothing without the
**seed, the count and the difficulty** — report all three. Different values are different benchmarks.

**`balanced_accuracy` is 0.5 and I thought I did well.** 0.5 is the trivial guesser. If
`accuracy_ignoring_replay` is much higher, the submission is asserting more than it can demonstrate.

**Exit code 3 from the CLI.** Misconfiguration — usually a missing `--tasks` file. It is deliberately
not 0: a scorer pointed at nothing must not report success.

**A `hard` set is slower than I expected.** Difficulty controls the *size of the search*, not how
tricky the answer is. `hard` means four components and wider bounds, so the state space grows.

## FAQ

**"A generated benchmark can't be as good as a curated one."**
Correct, and they are for different things. [`protocol-bench`](https://github.com/nickharris808/protocol-bench)
is fixed, small, drawn from published standards and human-reviewed — that is what you cite. Its
weakness is stated in its own README: 15 tasks with 2 violated means one task flipping moves balanced
accuracy by 0.25, and its answers age into training corpora. `specforge` cannot be memorised, but its
machines are synthetic. Use the first for a citable number and the second for a number you can trust
has not leaked.

**"How do I know the generated answer key is right?"**
Three rules, each enforced at generation time and each covered by a test: a task is emitted only on a
definite verdict; every violated task's counterexample is replayed against its own model before the
task is emitted; generation is deterministic from the seed. The test that matters most re-runs the
checker on every generated task and requires the stored label to match — if a label and its model
ever disagree, every score computed against that set is meaningless.

**"Why does a benchmark need traces? Isn't the verdict the answer?"**
Because the verdict is guessable and the trace is not. Measured here: a submission that knows every
answer and fabricates every trace scores **0.500**, exactly what the always-safe guesser scores,
while its `accuracy_ignoring_replay` is **1.000**. The gap between those two numbers is the
measurement.

**"So I can just report the best seed I found?"**
You can, and it would be meaningless, which is why every surface here asks for the seed and count
next to the score. A number nobody else can regenerate is not a result. If you are reporting
comparatively, fix the seed *before* you run anything.

**"Is `bfs` the thing to beat?"**
No. It is sound and complete over a model that has already been formalised for it, so it is the
ceiling by construction. The open problem is producing the same verdict *from a description* rather
than from a transition table.

**"Can I use this to evaluate a language model?"**
Yes, but note what it does and does not isolate: the model is given, so this measures formal
reasoning over an explicit machine, not specification reading. For the harder mode — a standards
clause and a description, with the transition table withheld — use `protocol-bench prompts
--mode spec`.

## Tests

```
pip install -e ".[test]" && pytest
```

82 tests. The important ones re-derive every label independently, replay every shipped
counterexample, and assert that a fabricated submission scores exactly what guessing scores.

## The portfolio

| | |
|---|---|
| [`minicheck`](https://github.com/nickharris808/minicheck) | The engine: an explicit-state model checker with a CLI. Shortest counterexamples, no required dependencies. |
| [`protocol-bench`](https://github.com/nickharris808/protocol-bench) | Published IEEE 802.11 / 3GPP procedures with ground-truth verdicts. A claimed detection must **replay**. |
| [`specforge`](https://github.com/nickharris808/specforge) ← *you are here* | A benchmark that cannot be memorised — ground truth is *computed* by the checker, not written down. |
| [`minicheck-mcp`](https://github.com/nickharris808/minicheck-mcp) | The checker as an **MCP server**, so an agent can verify a state machine instead of guessing. |
| [`minicheck-action`](https://github.com/nickharris808/minicheck-action) | Model-check every spec in a repo, in CI. Diagrams in the PR, SARIF in the Security tab. |
| [`protocol-bench-action`](https://github.com/nickharris808/protocol-bench-action) | Score a submission in CI and fail the build if a claimed detection cannot be proved by replay. |
| [`failclosed`](https://github.com/nickharris808/failclosed) | Default-deny ASGI middleware: a gated endpoint succeeds only on an affirmative verdict. |
| [`polyfrac`](https://github.com/nickharris808/polyfrac) | Exact polynomial and rational-function arithmetic over ℚ with Sturm real-root counting. Zero deps. |
| [**the docs site**](https://nickharris808.github.io/verification-docs/) | The front door: why a verdict you cannot check is not a verdict, and how these compose. |

One idea runs through all of them: **a verdict you cannot check is not a verdict** — and its
corollary, which governs every surface here: *undetermined is not a pass.*

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

## Documentation

Full documentation, including the concepts guide and an honest comparison against TLA+, SPIN, Alloy
and CBMC, is at **[https://nickharris808.github.io/verification-docs/](https://nickharris808.github.io/verification-docs/)**.

## Contributing

Bug reports and pull requests are welcome — see [CONTRIBUTING.md](CONTRIBUTING.md). A counterexample
that this tool gets wrong is the single most useful thing you can send.

## Citing

Citation metadata is in [CITATION.cff](CITATION.cff); GitHub renders a *Cite this repository* button
from it.

## Licence

MIT. See [LICENSE](LICENSE).