Dafny Program Verification on DafnyBench (test)
89.1Verification Rate (NoDiff)SEVerA
Evaluation results
| Method | Links | ||||
|---|---|---|---|---|---|
| SEVerAconstraints=NoDiff behavioral specification2026.03 | 89.1 | 89.1 | 0 | 25.6 | |
| DafnyBench baseline2026.03 | 81.6 | 84 | 8.2 | 20.1 | |
| SEVerA (w/o constraints)constraints=None2026.03 | 79.2 | 84.8 | 7.9 | 18.4 | |
| LLM (Claude Sonnet 4.5)Model=Claude Sonnet 4.52026.03 | 68.7 | 71.1 | 10.3 | 10.3 |