LiveFMBench - Pre2025: leaderboard
Metric: Pass@1 (%) after the faithfulness check on LiveFMBench-Pre2025 (270 C programs from AutoSpec, FMBench and GitHub), direct prompting (instructions plus the C program), 32 samples at temperature 0.7 and top-p 0.95, pass@1 estimated from the 32 samples with the unbiased estimator; a sample counts only when Frama-C/WP (Alt-Ergo and Z3) proves the program and its code and assertions are unchanged (faithfulness check); higher is better. Source: arxiv.org. Saturation forecast: Around January 2027. 15 models tracked.
Top models
| # | Model | Score |
|---|---|---|
| 1 | Qwen 3 235B A22B 2507 (Thinking) | 34.92 |
| 2 | DeepSeek R1 0528 | 34.69 |
| 3 | DeepSeek V3.1 Terminus (Thinking) | 30.52 |
| 4 | DeepSeek V3.2 (Thinking) | 30.31 |
| 5 | Kimi K2 0905 | 27.49 |
| 6 | Qwen 3 32B | 27.44 |
| 7 | GLM-4.6 | 27.08 |
| 8 | Qwen 3 Coder 480B A35B Instruct | 27.04 |
| 9 | DeepSeek V3.1 Terminus | 24.64 |
| 10 | DeepSeek V3.2 (Non-reasoning) | 23.24 |
| 11 | DeepSeek V3 (0324) | 19.47 |
| 12 | GLM-4.6 (Non-reasoning) | 17.15 |
| 13 | Qwen 3 235B A22B 2507 Instruct | 11.54 |
| 14 | Qwen 3 32B (Non-reasoning) | 6.33 |
| 15 | Llama 3.3 70B Instruct | 4.27 |
Interactive version: theaggregate.ai/benchmark?slug=livefmbench-pre2025 · How It Works · Data refreshed daily, snapshot 2026-10-07.