Rust Formal Verification Benchmark
Can AI prove properties of real Rust code?
Each task takes a property test that a Rust crate already ships and turns it into a Lean 4 theorem about the crate itself, translated to Lean by hax, Charon, and Aeneas. A model succeeds only if Lean accepts its proof.
Leaderboard
| # | Model | Solved |
|---|---|---|
| 1 | gemini-4-argon-eap | 87% |
| 2 | claude-opus-5.5 | 84% |
| 3 | gpt-6-astra | 75% |
| 3 | gpt-6.1-sol | 75% |
| 5 | glm-5.3 | 46% |
| 6 | glm-5.3-flash | 32% |
| 7 | grok-4.7 | 22% |
| 8 | muse-spark-1.3 | 16% |
| 9 | gpt-6-luna | 5% |
| – | muse-wonder-1.0partial | 26/53 tasks |
Share of the 100 tasks solved in a single run with a 50-turn budget. Tasks lost to provider errors count as failures. Partial runs finished fewer than 95 tasks and are not ranked. The top two models are within statistical noise of each other.
About the benchmark
The benchmark has 100 proof tasks from 33 open-source Rust crates: 21 easy, 47 medium, and 32 hard. The implementation is the crate itself, extracted mechanically. The specification is the maintainers' own property test: its inputs, assumptions, and assertions, plus the requirement that the code never panics.
Every task ships a reference proof. The model edits one proof file and may not change the theorem. The verifier rebuilds the file in a clean, sandboxed copy of the benchmark, pinned to Lean 4.31.0, and accepts it only if it uses no axioms beyond Lean's standard ones.
What we found
Checking that a proof uses only Lean's standard axioms is not enough when the author is an agent. Code that runs during elaboration can skip kernel checking, and a single submission passed all 100 tasks without proving anything. Replaying the compiled proof through the kernel rejects it. We replayed all 468 recorded passing proofs: no model exploited the gap.
Strong models split into two strategies. Some submit only when they are sure (all 84 of Claude Opus 5.5's solves passed on the first try); others submit early and iterate. Almost every failure ends at the turn limit, and weaker models spend more calls exploring per proof attempt.
Agents already use metaprogramming and prompt-forbidden tactics while exploring. A harness bug told agents 4,184 times that files containing sorry were clean, showing how much the environment shapes their behavior.
Every task, reference proof, verifier, and agent transcript is open source. See also the Ethereum Verification Benchmark.