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.1 is the current published baseline: 135 active tasks drawn from production protocols, standards, bridges, auctions, vaults, and security challenge contracts. Complete model rows are rankable; partial rows are retained for transparency.

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/	Fair harness, agent adapters, 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
• Harness internals
• Task API
• Results publication model
• Evaluation surface