Ethereum Verification Benchmark

AI agents proving Ethereum smart contract properties in Lean 4.

Leaderboard  ·  Committed results  ·  Run guide  ·  Evaluation surface  ·  Verity docs

---

What This Is

Ethereum Verification Benchmark is an open benchmark for measuring whether AI agents can produce machine-checked proofs of smart contract correctness.

Each task gives an agent:

• a fixed contract implementation,
• a fixed formal specification,
• one editable Lean proof file,
• one target theorem.

The agent passes only if Lean accepts the proof. The verifier rejects theorem changes, hidden imports, sorry, admit, axiom, and other benchmark-policy violations.

The suite uses Verity, a Lean 4 EDSL for modeling EVM smart contracts with a shallow embedding. Verity also provides a proven compilation pipeline backed by a deep embedding, but this benchmark does not exercise that pipeline.

The benchmark is maintained by LFG Labs in partnership with the Ethereum Foundation and ecosystem protocols.

Results

The public dashboard is lfglabs.dev/benchmark.

Committed result data lives in:

• leaderboard.md
• results/index.json
• results/leaderboards/
• results/manifests/
• results/summaries/

Version 0.3 is the current benchmark environment: 263 frozen tasks on Lean 4.31. New comparable model campaigns should use the reproducible v0.3 STRAT-50 panel. Version 0.1 remains the older public-dashboard baseline, while v0.2/Lean 4.24 artifacts remain frozen for historical reproduction only. Results from different benchmark versions or inference protocols are separate cohorts and must not be combined.

Quick Start

Verify one reference proof:

./scripts/run_task.sh ethereum/deposit_contract_minimal/deposit_count

Run one task through the fair default harness:

cp .env.example .env
$EDITOR .env
python3 -m harness.cli run-task ethereum/deposit_contract_minimal/deposit_count --harness default

Run the local checks used by CI:

python3 scripts/check.py

Repository Layout

Path	Purpose
cases/	Active benchmark cases and task manifests
backlog/	Runnable tasks not yet in the active suite
Benchmark/	Lean modules for contracts, specs, proofs, and shared Grindset lemmas
harness/	Canonical fair harness, metering, and verifier policy
scripts/	Verification, aggregation, release, and analysis tooling
benchmark-versions/	Version manifests and compatibility fingerprints
results/	Published result indexes, summaries, and leaderboards
docs/	Architecture, operation, and evaluation notes

Docs

• Run and publish benchmark results
• v0.3 STRAT-50 panel and campaign guide
• Harness internals
• Task API
• Results publication model
• Evaluation surface