Formal Verification Benchmark Demo

A runnable, 10-task sample of LFG Labs' Ethereum Verification Benchmark. It tests whether an AI agent can prove smart-contract properties in Lean 4—not merely explain why they might be true.

The demo covers seven protocol and contract families, three difficulty levels, and several proof types. It includes everything needed to run and check submissions, but no reference solutions.

Why we built this benchmark

LFG Labs secures production smart contracts with formal verification. We translate contract behavior into Lean 4 specifications, prove correctness across every execution path, and deliver proofs that anyone can re-check by machine. Our production work spans protocols, developer infrastructure, and machine-checked proofs for organizations including the Ethereum Foundation, StarkWare, Nexus Mutual, and the Internet Computer.

We also use AI in our verification workflow. General coding benchmarks do not tell us whether a model can reason soundly about invariants, state transitions, authorization, and arithmetic. Developed with support from the Ethereum Foundation, this benchmark measures the capability we actually need: producing a valid mathematical proof for a fixed contract model and specification.

The tasks come from production protocols and the same formal-verification process we use for client work. Each one is scoped and reviewed by a formal verification engineer, tied to pinned source code, and backed by a Lean-accepted reference proof. This gives us a quality-controlled pipeline we can extend for evaluation, training, or custom model-development partnerships.

How it works

Each task gives the model:

• a fixed Verity model of selected contract behavior;
• a fixed formal specification;
• one Lean theorem with an editable proof body;
• the same generic proof automation as every other participant.

The model passes only when Lean accepts the theorem. The checker rejects changed theorem statements, incomplete proofs, forbidden declarations, and hidden reference-proof imports. There is no partial credit and no judge model: Lean is the grader.

Demo tasks

Difficulty	Contract	Task	Property
Easy	Lido VaultHub	max_liability_shares_bound	Maximum liability shares remain bounded
Easy	ERC-4337 EntryPoint	no_execution_on_revert	Reverted validation prevents execution
Easy	Zama ERC-7984	transfer_preserves_supply	Confidential transfers preserve total supply
Medium	Safe OwnerManager	add_owner_is_owner_correctness	Adding an owner updates ownership correctly
Medium	1inch Aqua	quote_exact_in_curve_safety	Exact-input quotes preserve the swap curve bound
Medium	StarkGate	withdraw_preserves_escrow_lower_bound	Withdrawals preserve the bridge escrow lower bound
Hard	Lido VaultHub	locked_funds_solvency	Locked funds preserve modeled VaultHub solvency
Hard	Safe OwnerManager	add_owner_acyclicity	Adding an owner preserves linked-list acyclicity
Hard	Morpho Midnight	normal_mode_max_repaid_restores_health	Maximum permitted repayment restores health within rounding tolerance
Hard	Morpho Midnight	bad_debt_preserves_lender_credit_cover	Bad-debt slashing preserves lender-credit coverage

The Lido, Safe, 1inch, StarkGate, ERC-4337, and Zama tasks are selected directly from the benchmark. The Morpho tasks adapt the arithmetic statements from LFG Labs' pinned Midnight verification to this demo's Lean 4.24 environment.

The full machine-readable catalog is in demo-manifest.json.

Run the demo

Requirements: Linux or macOS, Git, Python 3.10+, and elan. The first setup downloads the pinned Lean dependencies and Mathlib cache.

git clone https://github.com/lfglabs-dev/formal_bench_demo.git
cd formal_bench_demo
./scripts/setup.sh
./scripts/list_tasks.py

Choose a task, replace only its proof body after := by, and run the checker:

$EDITOR Benchmark/Generated/Lido/VaulthubLocked/Tasks/MaxLiabilitySharesBound.lean
./scripts/check_task.py lido/vaulthub_locked/max_liability_shares_bound

An untouched task fails because ?_ is an incomplete proof. A valid submission prints:

Checking lido/vaulthub_locked/max_liability_shares_bound
PASS: Lean accepted the target theorem.

Restore a task with:

git restore Benchmark/Generated/Lido/VaulthubLocked/Tasks/MaxLiabilitySharesBound.lean

Repository structure

Path	Purpose
Benchmark/Cases/	Fixed contract models and specifications
Benchmark/Generated/	Ten editable proof tasks
Benchmark/Grindset/	Generic proof-normalization support; no task solutions
demo-manifest.json	Task metadata, pinned sources, and theorem hashes
scripts/setup.sh	Install dependencies and build the base project
scripts/list_tasks.py	List the demo tasks
scripts/check_manifest.py	Validate dataset metadata and theorem integrity
scripts/check_task.py	Check one submission with policy rules and Lean

The production harness adds isolated workspaces, complete task and environment fingerprints, usage metering, infrastructure-failure classification, and reproducible run artifacts.

Benchmark scale

	Frozen v0.1	Current suite
Runnable proof tasks	135	204
Protocol/case families	25	35
Contract implementations	25	36
Machine-checked reference proofs	135	204

Version 0.1 has 1,890 valid evaluations across 14 model configurations. The current suite contains 75 entry/easy, 99 medium, and 30 hard tasks after normalizing two legacy low labels.

The benchmark is strongest on accounting, state preservation, storage effects, control flow, ownership, authorization, rounding, and solvency. Priority additions are Aave V3 liquidations, Uniswap v4 hooks and settlement, EigenLayer slashing, Chainlink oracle transitions, and Morpho Blue accounting.

Reproducibility and scope

The demo pins Lean 4.24, Verity, all Lake dependencies, upstream contract revisions, task metadata, and SHA-256 hashes of every immutable theorem prefix. Each task models a reviewed protocol slice rather than the entire EVM system; its abstraction notes and Morpho proof provenance are recorded in demo-manifest.json.

Every full-benchmark task has a machine-checked reference proof, withheld from the evaluated model workspace.

Work with LFG Labs

See our formal verification research, benchmark results, and production work.

For full-benchmark access, custom data generation, model evaluation, training-data licensing, or smart-contract verification, contact us through lfglabs.dev.