Score a solver with every counterexample replayed

A claim without a trace that replays earns nothing. That is the only way to tell a solver which found a bug from one which guessed the label — and it is what this leaderboard measures.

Tasks are generated, not fixed, so nothing here can be memorised: change the seed and the answer key changes. Every label was computed by an exhaustive model checker, and a candidate the checker could not settle produces no task rather than a guessed one. Everything runs in this page; nothing is uploaded.

Starting the checker…

The fabricated-trace oracle, already scored

Perfect labels on every task. Every trace invented. Here is what it earns:

An oracle that knows every answer and fabricates every trace

Perfect labels. No evidence. Watch what it scores.

Balanced accuracy: 0.500

metric	value
tasks	20
balanced accuracy	0.500
accuracy	0.500
trivial always-safe accuracy	0.500
recall on violated	0.000
recall on safe	1.000
detections claimed	10
counterexamples that replayed	0
claims that did not replay	10
TP / FP / FN / TN	0 / 0 / 10 / 10

⚠️ Accuracy ignoring replay is 1.000, against 0.500 credited. This submission asserts more than it demonstrates — 10 claim(s) had no trace that replays.

By shape

shape	tasks	correct
`bounded_retry`	5	4
`handshake`	5	1
`mutual_exclusion`	3	1
`resource_pool`	3	1
`sequence_window`	4	3

Claims that were not credited, and why

task	reason
`sequence_window_medium_44`	a step does not name the fields ('seq', 'acked', 'aux0')
`mutual_exclusion_medium_46`	a step does not name the fields ('p0', 'p1', 'p2', 'lock', 'aux0')
`handshake_medium_48`	a step does not name the fields ('req', 'resp', 'installed', 'aux0')
`resource_pool_medium_50`	a step does not name the fields ('held', 'c0', 'c1', 'c2', 'aux0')
`handshake_medium_53`	a step does not name the fields ('req', 'resp', 'installed', 'aux0')
`resource_pool_medium_55`	a step does not name the fields ('held', 'c0', 'c1', 'c2', 'aux0')
`mutual_exclusion_medium_56`	a step does not name the fields ('p0', 'p1', 'p2', 'lock', 'aux0')
`handshake_medium_58`	a step does not name the fields ('req', 'resp', 'installed', 'aux0')
`handshake_medium_68`	a step does not name the fields ('req', 'resp', 'installed', 'aux0')
`bounded_retry_medium_72`	a step does not name the fields ('tries', 'done', 'aux0')

Run it yourself below, at any seed and size. The gap between accuracy_ignoring_replay and the credited accuracy is the whole measurement.

Task set

tasks seed difficulty

tasks.json — copy this and solve offline

Baselines

Three reference points. The third is the one worth looking at: perfect labels, fabricated traces. It scores what guessing scores, because it demonstrated nothing.

Score a submission

A submission maps task id to a prediction. violated is required; trace is what earns the detection — it must start at the initial state, move only along real transitions, and end in a state that genuinely violates the property.

{
  "mutual_exclusion_medium_3": {"violated": true,
                                "trace": [{"state": {"p0": 0, "p1": 0, "lock": 0}}, ...]},
  "handshake_medium_7":        {"violated": false}
}

submission JSON

Run the same scoring on your machine

pip install "pcar-specforge @ git+https://github.com/nickharris808/specforge.git"
specforge run bfs --n 20 --seed 42

Same generator, same seed, same answer key. Do not run pip install specforge — that name on PyPI belongs to an unrelated project (SGLang's SpecForge), so it succeeds and installs something else. The git+ form above is unambiguous.