Correction and apology — 1 September 2026
The earlier version of this page named the wrong machine. It said the model ran on a desktop with an eight-core Ryzen 7800X3D and two Radeon AI PRO R9700 cards. It did not. Every run described here happened on a MacBook Pro — Apple M5 Max, 48 GB. The Ryzen machine was never involved and served no part of it.
I am sorry. This site's argument is about what modest hardware can do,
most of the people reading it care a great deal about which hardware, and
I described the wrong one. There is no excuse for it. The run records
said host = Bill all along and I did not check them against
what I had written.
The headline number was also wrong. It said 25/26. The fitted run scored 24/26. The twenty-fifth was a task solved afterwards, outside the scored run, and folding it into the headline was not right.
And two different results were presented as one. The held-out run has two arms and they measure different things: 19/26 with the prompt frozen, 25/26 when the loop is allowed to rewrite it. Quoting only the larger number hid the comparison that makes the result interesting.
The page below is rewritten from the run records rather than corrected in place. Every figure has been recomputed. Nothing here is quoted from the earlier version.
Benchmark report · rewritten 1 September 2026
SPARK on the vericoding benchmark — what a 30B model did, and did not, do
Twenty-six formal specifications, a theorem prover as the only judge, and an open-weights model running on a laptop. This is what happened, with the figures set out so you can check them or skip them.
What was tested
Twenty-six tasks from the Beneficial AI Foundation's vericoding benchmark, translated one-for-one from Dafny into SPARK/Ada. SPARK carries its contracts in the language; GNATprove decides whether a body meets its specification.
Nothing in the scoring is a model. A pass is a discharged proof obligation. Code that compiles but cannot be proved fails. Code that does not compile fails. A wrong answer that reads well scores zero.
Setup
| Model | qwen3-coder:30b, Q4_K_M, 30.5B parameters, qwen3moe |
|---|---|
| Rail | ollama, localhost |
| Machine | MacBook Pro, Apple M5 Max, 18 cores, 48 GB |
| Temperature | 0.2 |
| Context | 16384 |
| Protocol | the benchmark's own — up to 5 attempts per spec, prover output fed back between attempts |
The same machine ran the inference and the prover.
Result 1 — the fitted ladder, 26 tasks
Prose was written, scored, rewritten from what failed, and scored again.
| Condition | Prose | Calls | Passed | Cumulative |
|---|---|---|---|---|
| the benchmark's own prompt | prompts-spark.yaml | 130 | 0 | 0 / 26 |
| round A — SPARK rules written blind | 7,173 B | 26 | 0 | 0 / 26 |
| round B — corrected after reading A's failures | 9,956 B | 26 | 19 | 19 / 26 |
| round C | 12.6 KB | 7 | 3 | 22 / 26 |
| round D | 14.7 KB | 4 | 2 | 24 / 26 |
| round E | 16.7 KB | 2 | 0 | 24 / 26 |
Independent re-verification of the final set: 24 / 24 pass, 351
proof obligations, 0 unproved, 0 justified. Never passed:
NpArgmax-spec, NpCumSum-spec. Zero cheat verdicts
across 130 attempts — no pragma Assume, no
SPARK_Mode => Off.
Where the time went
| Seconds | Minutes | |
|---|---|---|
| inference (65 calls) | 129.2 | 2.2 |
| GNATprove | 578.8 | 9.6 |
| total | 708.0 | 11.8 |
The prover took 4.5× longer than the model did.
Failure costs more than success
| Round A outcome | n | Mean prover time | Total |
|---|---|---|---|
| unproved | 16 | 23.5 s | 376.3 s |
| compile_error | 10 | 0.4 s | 4.2 s |
Round B passes averaged 2.6 s of prover time, its failures 4.1 s. Code that compiles but cannot be proved is the expensive case, because the prover exhausts its search before giving up.
Result 2 — held out on 26 unseen specs
Two arms, the frozen arm run first so the adaptive arm could not
contaminate it. The frozen prompt is byte-identical to round B above
(sha256 3873db3a848f…).
| Arm | Condition | Passed |
|---|---|---|
| frozen | round-B prose unchanged, 1 attempt per spec, no feedback | 19 / 26 |
| adaptive | prose rewritten between rounds | 25 / 26 |
| Adaptive round | Calls | Passed | Cumulative |
|---|---|---|---|
| B (frozen prose) | 26 | 19 | 19 |
| F1 | 7 | 4 | 23 |
| N1 | 3 | 1 | 24 |
| N2 | 2 | 0 | 24 |
| N3 | 2 | 1 | 25 |
Across the arm: 25 pass, 7 unproved, 8 compile_error. Never passed in-run:
NpArgmin-spec.
One result is excluded. NpArgmin-spec was
solved later, which would have made the adaptive arm 26 / 26.
It is not counted. The prose that reached it was written after a
known-good answer had been read here, so the task was no longer held out.
Seven adaptive gains were achieved and six are counted.
Four of the 26 held-out tasks were close relatives of tasks the prose had already seen. Excluding those four: frozen 15 / 22, full process 21 / 22.
Result 3 — the benchmark's harder tier
| Arm | Passed |
|---|---|
| frozen, 1 attempt | 1 / 26 |
| adaptive, full container plus a new-rule round | 1 / 26 |
The denominator is not 26. Nine of those tasks look unwinnable as
translated: their non-editable preambles leave overflow, range and
Subprogram_Variant obligations on the specification functions
themselves, and no body can discharge those. The honest denominator is 17
or lower — so 1 / 17, which does not rescue it.
The generalisation seen at the easier difficulty does not appear here.
For comparison — the same 26 tasks in Dafny
From the benchmark's own shipped results file.
| Model | Passed | Weights |
|---|---|---|
| gpt-5-mini | 23 / 26 — 88.5% | closed |
| gemini-2.5-pro | 23 / 26 — 88.5% | closed |
| claude-sonnet-4 | 23 / 26 — 88.5% | closed |
| claude-opus-4.1 | 23 / 26 — 88.5% | closed |
| gpt-5 | 22 / 26 — 84.6% | closed |
| glm-4.5 | 20 / 26 — 76.9% | open |
| grok-code | 19 / 26 — 73.1% | closed |
| gemini-2.5-flash | 19 / 26 — 73.1% | closed |
| deepseek-chat-v3.1 | 15 / 26 — 57.7% | open |
| all nine | 187 / 234 — 79.9% |
Those runs used up to five attempts per task with prover feedback. The frozen arm above used one attempt and no feedback.
Limits
This is not a SPARK-versus-Dafny comparison. Two variables moved together, the language and the model class. No frontier model has been run against the SPARK seed set.
The attempt budgets differ. The frontier figures are five attempts with feedback; the frozen arm is one attempt without.
Two of those nine may be published below their capability.
deepseek-chat-v3.1 is the non-thinking variant, and nothing in
the benchmark repo states whether GLM-4.5's thinking mode was enabled.
Both are the open-weight entries. I have asked and do not yet know.
The benchmark's own headlines do not all reproduce from the results file it ships. Dafny 82% computes to 83.1%; Verus 44% computes to 31.1%; Lean 27% computes to 18.0%.
No energy figure is reported, because none was measured. The telemetry recorded load average and temperature, not power, and inference and proving ran on the same machine, so no clean figure can be taken from this run. Measuring it properly means measuring it elsewhere, on somebody else's meter, with the proving kept separate. That is the next experiment and the number will be published whichever way it goes.
None of this is a leaderboard number. Hand-written prose is not legal under the benchmark's own protocol, which requires a fixed per-language prompt not of the entrant's choosing. These figures sit beside the benchmark, not in it.
One model, one quantisation, one machine. Nothing here has been reproduced on other hardware or another backend.
Conclusion
An open-weights model of thirty billion parameters, given the benchmark's own prompt, discharged 0 of 26.
The same model, same weights, same quantisation, same machine, given a fixed 9,956-byte prompt describing the idiom it was failing on, discharged 19 of 26 on specifications that prompt had never seen, at one attempt each and no feedback.
The variable that changed was prompt content. Model, hardware and attempt budget were held constant.
The effect is bounded by difficulty. Against the benchmark's harder tier the same fixed prompt discharged 1 of 17.
Check it
Everything above is reproducible from the published evidence — specifications, the frozen prompt with its checksum, the harness, the verifier, the negative control, the record of a cheat attempt, and per-specification results for every condition.
github.com/the-dark-factory/spark-benchmark-evidence
Clone it, run spark_verify.py --level=2, and knock any of it
down if it does not hold.