Results · Model bench
Models, scored by the prover.
A fixed battery of 21 SPARK package specifications. For each spec, a
model gets up to three attempts to write the implementation body. A
pass means the body compiled and every proof obligation was
mathematically discharged by gnatprove — and then
the whole proof was re-run from scratch, independently, before the
score was recorded. There is no self-reporting anywhere in the chain,
and a machine-checked gate rejects bodies that try to assume their
way past a proof.
The table
| Model | Route | Date | Honestly proven | Notes |
|---|---|---|---|---|
| claude-fable-5 | frontier API (Anthropic) | 2026‑07‑18 | 20/21 | the only model to pass the battery’s hardest proof (first attempt); its sole fail was the item since confirmed as our own battery defect — run on a flat-rate plan, so per-run token cost is not separately metered |
| kimi-k3 | provider API (Moonshot) | 2026‑07‑18 | 19/21 | same score and same two fails as its code-tuned sibling, at roughly three times the token cost (£0.46); sampling temperature likewise fixed at 1 by the API |
| kimi-k2.7-code | provider API (Moonshot) | 2026‑07‑18 | 19/21 | first provider-hosted row; sampling temperature fixed at 1 by the API (see caveats); whole run cost £0.14 in tokens; its two fails are the battery’s two hardest items — one was later confirmed as a defect in our own battery, fixed in battery v2 (see below) |
| qwen3.6-27b | open weights, on‑premises | 2026‑07‑16 | 17/21 | score reproduced exactly on a second full run the same day |
| qwen2.5-coder-32b | open weights, on‑premises | 2026‑06‑26 | 14/21 | |
| qwen3-coder-30b | open weights, on‑premises | 2026‑06‑26 | 10/21 |
The table lists every outside model benched on this battery to date. Scores are not comparable with any other benchmark's numbers: this battery scores proof, not plausibility.
What a pass costs a model
Each spec carries contracts — preconditions, postconditions,
invariants. The model's body must satisfy all of them under
gnatprove --level=2: no unproven obligations, no
warnings waved through. A separate, itself formally proven, gate
then inspects every discharged body for proof-bypass constructs
(pragma Assume, disabled analysis modes, axiomatised
imports) and fails the candidate if it finds one. What survives is
code that is proven to meet its specification — the
standard our factory holds its own output to.
Caveats, stated plainly
- Sampling regimes differ where a provider forces them to. On-premises rows sample at the bench-standard low temperature. Moonshot's API rejects any temperature except 1 for kimi models, so the kimi row necessarily samples differently. Same specs, same prover, same gate — but not an identical sampling regime.
- Provider-hosted rows leave the building. The battery's specs transit the provider's cloud for those rows. Nothing else does: the battery is a fixed public-shape fixture set, not customer material.
- Three attempts per spec, no human help, no hints from a stronger model. Retries see only the prover's own error output.
- When we get it wrong, we say so. The bench has previously corrected a harness defect that unfairly marked two models down, by name, in the open. That policy stands.