VeriContest - SpecGen: leaderboard
Metric: Specification generation pass@1 (%): share of problems whose Verus specification generated from the natural-language description (nl2spec) is accepted as equivalent to the ground truth (sound and complete pre- and postconditions, checked with Verus proofs and negative tests), on the 946 VeriContest competitive-programming problems (690 LeetCode, 256 Codeforces) in Rust with Verus, one-shot prompting with a Verus-Bench example, temperature 0 where the API exposes it (provider default for GPT-5.5 and Claude Opus 4.7); higher is better. Source: arxiv.org. Saturation forecast: Around January 2027. 10 models tracked.
Top models
| # | Model | Score |
|---|---|---|
| 1 | GPT-5.5 | 48.31 |
| 2 | Claude Opus 4.7 | 20.82 |
| 3 | Gemini 3.1 Pro (Preview) | 19.03 |
| 4 | Gemini 3 Flash (Preview) | 14.59 |
| 5 | Claude Sonnet 4.6 | 13.11 |
| 6 | DeepSeek V4 Pro | 7.93 |
| 7 | DeepSeek V4 Flash | 4.77 |
| 8 | GPT-5.4 Mini | 2.36 |
| 9 | GLM-4.7 Flash | 1.48 |
| 10 | Qwen 3.6 27B | 0.32 |
Interactive version: theaggregate.ai/benchmark?slug=vericontest-specgen · How It Works · Data refreshed daily, snapshot 2026-10-07.