A curated list of awesome Ethereum formal verification tools, projects, and resources
Formal verification is a mathematical approach to proving the correctness of smart contracts and blockchain protocols. This list focuses on formally verified Ethereum-related projects, tools, and academic research.
- Awesome Ethereum Formal Verification
| Name | Category | Formal Verification | Stack |
|---|---|---|---|
| KZG Commitment | Commitment Scheme | ✅ | Isabelle/HOL |
| Merkle Tree | Commitment Scheme | 🏗️ WIP | Lean |
| Binius | Commitment Scheme | 🏗️ WIP (ring-switching + Binary Basefold proved; FRI-Binius in progress) | Lean |
| Sumcheck | Interactive Oracle Proof | 🏗️ WIP (full-protocol soundness landed; knowledge-soundness bridge pending) | Lean |
| FRI | Interactive Oracle Proof | ✅, ✅ (RBR soundness) | Lean |
| Batched FRI | Interactive Oracle Proof | 🏗️ WIP | Lean |
| STIR | Interactive Oracle Proof | 🏗️ WIP | Lean |
| WHIR | Interactive Oracle Proof | 🏗️ WIP | Lean |
| Spartan | Interactive Oracle Proof | 🏗️ WIP | Lean |
| XMSS (leanSig) | Signature Scheme | ✅ (SUF-CMA in the ROM) | Lean |
| SPHINCS+ (leanSPHINCS) | Signature Scheme | ✅ (SUF-CMA in the ROM) | Lean |
| Poseidon2 (Plonky3 AIR) | Hash Function | ✅ (constraint soundness) | Lean |
| Keccak (Plonky3 AIR) | Hash Function | ✅ (determinism and correctness) | Rocq |
| Keccak / SHA-2 (OpenVM) | Hash Function | ✅ (chip soundness) | Lean |
| Name | Category | Formal Verification | Stack |
|---|---|---|---|
| Ethereum PoS | L1 | ✅, ✅ (archived) | Rocq, Dafny |
| Casper FFG | L1 | ✅ | Rocq |
| Gasper | L1 | ✅ (bounded model checking) | TLA+, Apalache |
| 3-Slot Finality (3SF) | L1 | ✅ (Accountable Safety, bounded model checking) | TLA+, Apalache, CVC5, Alloy |
| RANDAO | L1 | ✅ | Maude, PVeStA |
| Staking deposit contract | L1 | ✅ | K Framework |
| Consensus specs (Fulu, Gloas, Heze) | L1 | 🏗️ WIP | Lean |
| leanSpec (Lean Consensus) | L1 | 🏗️ WIP, 🏗️ WIP (Verity client) | Lean |
| EIP1559 | EIP | ✅ | UPPAAL |
| Cairo (language) | zkVM (language) | ✅ | Lean |
| leanVM | zkVM | 🏗️ WIP (verifier knowledge soundness on the FV branch) |
Lean |
| Jolt | zkVM | 🏗️ WIP (bytecode expansion proved), 🏗️ WIP | Lean |
| SP1 | zkVM | ✅ (RV64 core chips), ✅ (determinism) | Lean, Picus |
| OpenVM | zkVM | ✅ (RV32IM chips) | Lean |
| Pico | zkVM | ✅ (RV32IM / RV64IM chips) | Lean |
| RISC Zero | zkVM | 🏗️ WIP (determinism), 🏗️ WIP (archived PoC) | Zirgen, Lean, Picus |
| Intmax2 | Zk Rollup | ✅ | Lean |
| CBC Casper | (L1) | ✅ | Isabelle/HOL |
| Name | Category | Formal Verification | Stack |
|---|---|---|---|
| Uniswap V3 | DEX | ✅ | Isabelle/HOL based custom tool |
| Uniswap V4 | DEX | ✅ | Certora Prover |
| Compound V3 | Lending | ✅ | Certora Prover |
| Euler Finance V2 | Lending | ✅ | Certora Prover |
| DJED | Stablecoin | ✅ | LUSTRE, Isabelle/HOL |
| AMM | DEX | ✅ | Lean |
| Morpho Blue | Lending | 🏗️ WIP | Verity (Lean) |
- EVMYulLean - Executable formal model of the EVM and Yul in Lean 4 (blog)
- KEVM - Executable EVM semantics in the K Framework
- evm-sail - Formal, executable EVM specification written in Sail, exportable to Lean, Rocq, Isabelle and HOL4 (WIP)
- evm-equivalence - Per-opcode equivalence proofs between EVMYulLean and KEVM in Lean 4 (WIP)
- Etheorem - Executable Lean 4 implementation of the consensus specs (Fulu, Gloas, Heze), tested against
consensus-spec-tests - formal-leanSpec - Lean 4 formalization of the Lean Consensus specification (leanSpec)
- riscv-zkvm - Lean extraction of the official Sail RISC-V specification for zkVM verification, built on the Lean backend for Sail
- Certora Prover - Formal verification tool for EVM, Solana, and Stellar chains, open source since February 2025
- K Framework (KEVM) - Ethereum verification using K specifications
- Kontrol - Formal verification of Foundry tests using KEVM
- halmos - Symbolic testing tool for EVM smart contracts
- HEVM - Symbolic EVM for symbolic execution, equivalence checking and formal verification
- SMTChecker - SMT-based formal verification module built into the Solidity compiler
- Act - Formal specification language for Ethereum smart contracts
- Verity - Lean 4 EDSL for EVM smart contracts with a machine-checked compiler to Yul (docs)
- Isabelle/Solidity - Shallow embedding of Solidity in Isabelle/HOL with a verification condition generator (see also the deep embedding)
- rocq-of-solidity - Formal verification of Solidity smart contracts in Rocq
- rocq-of-python - Converts Ethereum's Python specifications to Rocq (Coq) for formal verification (paused)
- Mythril - Symbolic-execution-based security analysis tool for EVM bytecode
- solc-verify - Modular verifier for Solidity smart contracts based on Boogie (no updates since 2023)
- Picus - Automated verification of the uniqueness (determinism) property of ZK circuits
- clean - Lean 4 DSL for writing and verifying ZK circuits (blog)
- zkLean - Lean 4 DSL for ZK statements, with an extractor for Jolt
- LLZK - MLIR-based intermediate representation for ZK circuits
- CertiPlonk - Extraction and verification of Plonky3 constraint systems in Lean
- Garden - Formal verification of ZK circuits in Rocq
- zkvm-verus - Evaluation of Verus for zkVM/zkEVM verification
- VeIR - Verified MLIR-style compiler infrastructure in Lean, aimed at a verified ZK compiler toolchain
- ArkLib - Formally verified interactive oracle reductions and SNARK components in Lean
- VCVio - Lean framework for machine-checked cryptographic security proofs
- CompPoly - Computable polynomials in Lean
- iris-lean - Lean 4 port of the Iris separation logic framework
- Microsoft VeriSol - Formal verifier for Solidity smart contracts (archived)
- Manticore - Symbolic execution tool for smart contracts (archived)
- Clear - Lean framework for verifying Yul programs (archived)
- Certora Security Reports - Comprehensive formal verification and audit reports for major Web3 protocols
- Runtime Verification Reports - Formal verification reports for blockchain projects
- Trail of Bits Publications - Security research and formal methods applications
- Ethereum Formal Verification Overview - Comprehensive overview of formal verification in the Ethereum ecosystem
- Verified zkEVM Project - Ethereum Foundation initiative funding formal verification of zkVMs, EVM implementations, and proof systems
- EthBench - Formal verification benchmark for Ethereum smart contracts (no updates since 2017)
- Awesome Web3 Formal Verification - Curated list of Web3 formal verification resources
- A Survey of Smart Contract Formal Verification - Comprehensive survey of formal verification techniques
- Jolt-QED: Formally Verifying Bytecode Expansions In Lean (2026) - Lean proofs of Jolt's RISC-V bytecode expansions
- Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis (2026) - VeriSynth: LLM-generated Python/Z3 models of Rust zkEVM opcode handlers
- A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report (2026) - Aeneas/Hax + ArkLib + AI provers applied to Plonky3 and RISC Zero primitives
- Verity: A Verified Compiler for a Core Fragment of EVM Smart Contracts in Lean 4 (2026) - Verified compilation chain from a Lean EDSL to Yul
- A Simplified Round-by-round Soundness Proof of FRI (2025) - Simplified RBR soundness proof of FRI, formalized in Lean (blog)
- Technical Report: Exploring Automatic Model-Checking of the Ethereum specification (2025) - Model checking Accountable Safety of 3SF with TLA+/Apalache
- Formal verification of safety properties of epoch processing in Beacon Chain (2025, Scientific Reports) - Model checking of Beacon Chain epoch processing
- Formal Verification of Rewards and Penalties Mechanism of FFG Attestations: Ethereum 2.0 Beacon Chain Case Study (2025, IEEE Access)
- Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL (2025, Formal Aspects of Computing) - Executable denotational semantics of Solidity
- Certified Decision Procedures for Width-Independent Bitvector Predicates (OOPSLA 2025) - Verified bitvector automation in Lean
- Interactive Bitvector Reasoning using Verified Bit-Blasting (OOPSLA 2025) - Verified bit-blasting in Lean
- Reentrancy Verification - Reentrancy attack verification using Z3 SMT solver
- SmartScan - Formal verification framework detecting 14 types of vulnerabilities
Contributions are welcome! Please follow the guidelines below.
- Quality over quantity - Only include high-quality, actively maintained projects
- Provide descriptions - Each entry should have a clear, concise description
- Verify links - Ensure all links are working and point to the correct resources
- Follow format - Maintain consistent formatting throughout the list
- Stay relevant - Focus on Ethereum and EVM-compatible formal verification
- Fork this repository
- Create a new branch for your additions
- Add your entry in the appropriate section
- Ensure your addition follows the format
- Submit a pull request with a clear description
To the extent possible under law, the contributors have waived all copyright and related or neighboring rights to this work.
Note: This list is continuously updated. If you find any broken links or outdated information, please open an issue or submit a pull request.