specforge¶
A benchmark that cannot be memorised
Generates protocol-shaped verification tasks whose ground truth is computed by an exhaustive checker rather than written down. Change the seed and nothing has seen the task set.
:material-github: Source :material-database: Dataset :material-trophy: Leaderboard
77 tests · ~741 lines of source · MIT
Install¶
Note
pip install specforge does not work yet — nothing here is on PyPI. Install from GitHub.
Honest scope¶
Reproduced from the package README, which is the source of truth.
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, 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.
Full documentation, quickstart and troubleshooting live in the repository README.