Ethereum Verification Benchmark
Evaluating AI deductive reasoning for Smart Contracts.
We evaluate frontier models on fresh problems derived from production Ethereum contracts. Each task pairs a Verity contract model with a fixed formal specification. A model succeeds only if it produces a proof accepted by Lean.
Leaderboard
| # | Model | Pass rate |
|---|---|---|
| 1 | gpt-5.6-sol | 34.0% |
| 2 | kimi-k3 | 28.0% |
| 3 | muse-spark-1.2 | 20.0% |
| 4 | gpt-5.6-terra | 20.0% |
| 5 | gpt-5.6-luna | 18.0% |
| 6 | minimax-m3 | 14.0% |
| 7 | glm-5.3 | 14.0% |
Pass rate is the share of proofs that compiled against the fixed specification. Each cohort has 50 terminal verdicts on the same STRAT-50 panel under the p4_normal budget of 16 attempts and 120 tool calls; infrastructure-invalid attempts are excluded. The table lists the highest-scoring completed cohort per model family, out of 12 completed cohorts.
Scaling Law
We re-ran MiniMax M3 on 50 tasks solved by the frontier model with steadily larger effort budgets. Its solve rate climbs from 12% to 96%, approaching a near-perfect rate as effort grows.
About the benchmark
The benchmark was developed with support from the Ethereum Foundation as part of our work to make formal verification of smart contracts more practical. Instead of asking a model to explain whether a contract is safe, Verity asks it to produce a mathematical proof that a specific formal property follows from a specific contract model and specification.
Version 0.2 contains 240 proof tasks from 37 deployed or ecosystem-relevant Ethereum cases. Each task includes a reference proof and a frozen grading setup. The model may attempt the proof, but it may not change the theorem statement or specification.
The leaderboard scores STRAT-50, a deterministic 50-task panel drawn from that manifest. It reports the observed solve rate on the panel, not an unweighted estimate of full 240-task performance.
A proof is considered correct only if it is accepted by the Lean 4 kernel, with no additional assumptions. Version 0.2 is pinned to Lean 4.24.0.
The frozen manifest, per-cohort run bundles, and SHA-256 checksums for this version are published in the v0.2 release.
Every task, specification, and grading harness is open source. Results are fully reproducible.
In collaboration with
Morpho
