I have been working in the Beneficial AI Foundation’s vericoding benchmark — the one where a theorem prover, not a test suite, decides whether the model’s code is right. I put the SPARK/Ada track into it, and I posted my own numbers here earlier.
While pulling their shipped results apart for a comparison, something stopped me, and I cannot answer it from the repo.
Restricted to the 26 numpy_simple
tasks I was working with, in Dafny:
| 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% |
The two open-weight entries are bottom and sixth. Those are the two anyone here could actually self-host, so they are the two I care about most.
Here is what I cannot resolve.
The DeepSeek entry is deepseek-chat-v3.1. V3.1 is a hybrid — it has a thinking mode and a non-thinking mode, and
chat
is the one with reasoning off. It is being scored against gpt-5, gemini-2.5-pro and claude-opus-4.1, which are reasoning models running as reasoning models.GLM-4.5 also has a thinking mode, and I cannot find anything in the repo that says whether it was enabled.
If both were run with the thing that makes them competitive switched off, then two open-weight models have been published at scores that are not what they can do, on a table people have been quoting since as a fair fight. I want to be careful here: I do not know that this is what happened. I am asking because I cannot find the run configuration recorded anywhere, and the model names are the only evidence I have.
What makes me want an answer rather than assume one is that the repo’s own headline numbers do not all reproduce from the results file it ships. Computing from their CSV:
| language | their headline | computes to |
|---|---|---|
| Dafny | 82% | 83.1% ✓ |
| Verus | 44% | 31.1% |
| Lean | 27% | 18.0% |
Dafny lands. The other two do not. That is not an accusation of anything, but it does mean I would rather ask than infer.
So, two questions for anyone who knows more than me.
If someone has hardware to serve either of them at a sensible quantisation, the test is cheap and entirely public: the same 26 Dafny tasks, their verifier, thinking on. I have neither the hardware nor a reason to be trusted as the only person running it, so I would rather it were somebody else, or several of us. Worth saying that this cuts against my own post. I have been describing my 30B local result as landing above both open-weight entrants. If those two come out in the eighties when run properly, that line of mine is wrong and I would want to know now rather than after I have said it a few more times.