Coding benchmarks did not match what we were seeing when using LLMs for formal verification. So we built our own. Today we’re releasing Ethereum Verification Benchmark V2

240 smart-contract verification tasks across 37 Ethereum cases, checked by the Lean 4 kernel. This is not a benchmark for explaining why a contract may be safe. Each task fixes the contract model, formal specification, and theorem statement. The agent only succeeds if Lean accepts the proof. Read more: veritylabs.dev/benchmark

Along the way, we found something even more interesting. With enough effort, smaller models replicated 96% of the tasks solved by frontier models. The scaling-law sidecar remains a useful view of how inference effort changes proof solve rate.