The vericoding benchmark (spec in, prover-accepted code out) covers Lean, Dafny and Rust/Verus. It had no Ada or SPARK track, so I have added one: Add a SPARK / GNATprove language track - Pull Request #320 - Beneficial-AI-Foundation/vericoding - GitHub
The track ships 26 specs translated from their Dafny set, reference solutions that all discharge at level 2 (387 obligations, none unproved), a gnatprove harness, and a negative control that rejects wrong bodies, pragma Assume, SPARK_Mode => Off and syntax errors. It also fails any submission where gnatprove emitted no checks at all - a mistake I made once and would rather nobody repeated.
Results, on my own desktop (qwen3-coder 30B, one Radeon R9700, no cloud)
- Model alone, their protocol of 5 attempts with prover feedback: 0/26. Every failure the same missing array initialisation, though 22 of 26 wrote a sound loop invariant.
-
- Same model given a short prose description of the idiom, with rounds that improve the prose rather than the code: 25/26. Frozen prose, one attempt each: 19/26.
-
- For scale, nine frontier models average 79.9% on the same tasks in Dafny.
- The caveats matter more than the number. One good prompt with no loop got 19 of those 25. Four of the remaining six came from prose written for earlier work rather than anything learned on the night. Four of the held-out tasks were near-relatives of ones the prose had seen, so without them it is 15/22 and 21/22. And one of the two hard tasks (index of maximum) was only cracked after somebody read a known-good answer, so it is not counted.
- I have been reading this group’s ancestors since 1999 and using Ada since 1987. SPARK deserved to be in that comparison and nobody had put it there. Corrections to the translations are very welcome - if a spec is unfaithful I would rather hear it here.
Full write-up: SPARK in the vericoding benchmark — The Dark Factory