Correction — 30 August 2026
We published this piece with a held-out score of twenty-five out of twenty-six. That held-out set was written by an agent we briefed, matched to the difficulty of the original twenty-six tasks. It was a fair test of whether the frozen prose generalises across tasks, and it passed.
Since then we ran the same frozen prose against a different held-out set: twenty-six tasks cloned from the benchmark's own repository, at the benchmark's own harder tier. The frozen prose scored one out of twenty-six. A further round of adaptation on top of it also scored one out of twenty-six.
Nine of those twenty-six turn out not to be winnable as translated — their non-editable sections carry proof obligations no body can discharge, so the honest denominator is at most seventeen. That makes it one out of seventeen, not one out of nine. It softens the number. It does not rescue it.
On that harder tier, frontier models in Dafny score 33.8%, down from 79.9% on the easy tier — they keep 0.42 of their easy-tier rate. Our frozen prose keeps 0.05 of its own. We do not just fall because the tasks are harder. We fall much faster than frontier models do on the same material.
What this means: the frozen prompt generalises across tasks of the same difficulty. It does not generalise across difficulty tiers. It encodes one shape of problem — a loop filling an array, with an invariant that mirrors the postcondition over what has been processed so far. Inside that shape it transfers cleanly. Outside it, it has nothing to say, and the model does not either.
The numbers below are the easy-tier numbers from the original piece and the original held-out run. They stand as measured. Read them alongside this correction, not instead of it.
Benchmark report · 30 August 2026
SPARK is in the benchmark now — 25/26 on easy tasks, 1/26 on hard ones
There is a benchmark for getting an LLM to write code that a prover will accept. Lean is in it, Dafny is in it, Rust with Verus is in it. Ada and SPARK were not in it, so we have put them in. The pull request is up and the rest of this is what we found while doing it.
The model on its own gets nothing
We took twenty-six of the benchmark's own tasks, translated them into SPARK as faithfully as we could, and handed them to qwen3-coder. That is a thirty-billion-parameter open model, and it was running on a desktop machine here in South Shields — an eight-core Ryzen 7800X3D with two Radeon AI PRO R9700 cards in it, though only one card was doing anything. Ordinary parts, bought outright. Five attempts per task with the prover's complaints fed back between attempts, which is what the benchmark asks for.
It scored nought out of twenty-six.
The failure was the same one every time: it never initialised the array it had been handed. That is not ignorance of proof, because twenty-two of the twenty-six wrote a perfectly reasonable loop invariant. It just did not know this particular idiom.
The same model inside our process gets twenty-five
Then we ran the same twenty-six the way we actually work here. A short piece of prose that describes the idiom, the model forging the body, gnatprove judging it, and rounds where what gets improved is the prose rather than the code. No one wrote a line of Ada by hand at any point.
Twenty-five out of twenty-six on tasks the prose had never seen. With the prose frozen and one attempt per task it was nineteen.
For comparison, nine frontier models average 79.9% on the same tasks in Dafny, and the best four average 88.5%.
What is wrong with our own numbers
We spent a while trying to knock holes in this and found several worth reporting.
Most of the gain is not our loop. A single well-written prompt with no loop at all got nineteen of the twenty-six. Everything else — the rounds, the seat rewriting prose between them — was worth six more.
Most of the rest is not learning either. Of the six extra tasks the full process cleared, four were solved by prose the factory already had sitting in its container from earlier work. Only two came out of anything discovered on the night.
And the fact that broke the plain run — initialise the array — was already in the plain prompt, worked example included. What our process added was emphasis rather than information, which is a less impressive thing to have added.
One failure kept coming back through four different attempts at a prompt rule and then went away immediately when we told the model where on the page to put the line. Something that responds to position and not to explanation should not be in a prompt at all, so that one is going into a rewriter instead.
Four of the twenty-six held-out tasks turned out to be close relatives of ones the prose had already seen. Leaving those out, the frozen figure is fifteen out of twenty-two and the full process is twenty-one out of twenty-two.
Two tasks beat us outright: a cumulative sum, and finding the index of the largest element. The four best frontier models fail those same two in Dafny. We went back and cracked both afterwards, but for the second one the prose was written after somebody read a known-good answer, so we are not counting it and we would rather say why than quietly bank it.
We picked the language that was built for this
SPARK's contracts are part of Ada rather than a separate proof layer, so the model writes one artefact instead of two and the prover argues back in ordinary Ada. That is forty years of a language designed for exactly this job and it is an advantage. I am not going to pretend it is not.
It has been available to everybody the whole time and nobody in that benchmark had taken it up, which says more about fashion than about anything else. And it did not do the work on its own, or the plain run would not have scored nought.
How to check it
Published at github.com/the-dark-factory/spark-benchmark-evidence: the specs, the frozen prompt with its checksum, the model with its digest, the judge with its digest, and every transcript including the failures. The caveats are the first thing in that repository, before any score. One set of transcripts is missing and named as missing: the naked baseline's generated code was written to a scratch directory and not kept, so re-running it is the first thing an auditor should do. The judge is gnatprove at level two with cheat-checks armed, and it fails anything that proves nothing at all. That last rule is there because we once had a run come back green having generated no checks to fail, which took a while to notice.
The claim is a narrow one. A thirty-billion-parameter open model, on hardware you can buy in a shop, inside a discipline that carries proofs, matches or beats frontier models at writing verified code, and it is the discipline doing most of that rather than the model.
The track is at github.com/Beneficial-AI-Foundation/vericoding, pull request 320.
Who did what
The Dark Factory is one man and a fair amount of machinery. Some of that machinery is AI, and it worked on this alongside me. Claude wrote the prose the model was given, drove the runs, built the harness, and turned up most of the awkward facts in the section above, including the ones that make our numbers look worse. It also keeps the memory of the place, which is the part I would miss if it went away.
I am saying so for the same reason the failures are in here. If the argument is that the discipline does the work and the tools are interchangeable, then hiding which tools were used would be a strange way to make it. The decisions were mine and the errands were shared, and gnatprove did not care either way.