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 | Lean |
| Sumcheck | Interactive Oracle Proof | 🏗️ WIP | Lean |
| FRI | Interactive Oracle Proof | 🏗️ WIP | Lean |
| STIR | Interactive Oracle Proof | 🏗️ WIP | Lean |
| WHIR | Interactive Oracle Proof | 🏗️ WIP | Lean |
| Spartan | Interactive Oracle Proof | 🏗️ WIP | Lean |
| Name | Category | Formal Verification | Stack |
|---|---|---|---|
| Ethereum PoS | L1 | ✅, ✅ | Rocq, Dafny |
| Casper FFG | L1 | ✅ | Rocq |
| RANDAO | L1 | ✅ | Maude, PVeStA |
| Staking deposit contract | L1 | ✅ | K Framework |
| EIP1559 | EIP | ✅ | UPPAAL |
| Cairo (language) | zkVM (language) | ✅ | Lean |
| Jolt | zkVM | 🏗️ WIP | Lean |
| SP1 | zkVM | 🏗️ WIP | Picus |
| RISC Zero | zkVM | 🏗️ WIP | Zirgen, Lean |
| 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 |
- Certora Prover - Advanced formal verification tool for EVM, Solana, and Stellar chains
- Microsoft VeriSol - Microsoft's formal verifier for Solidity smart contracts
- K Framework (KEVM) - Ethereum verification using K specifications
- Coq-of-Python - Converts Ethereum's Python implementation to Rocq(Coq) for formal verification
- Act - Formal specification language for Ethereum smart contracts
- HEVM - Ethereum Virtual Machine for symbolic execution and formal verification
- Manticore - Symbolic execution tool for analysis of smart contracts
- Mythril - Security analysis tool for Ethereum smart contracts
- 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
- EthBench - Formal verification benchmark for Ethereum smart contracts
- Awesome Web3 Formal Verification - Curated list of Web3 formal verification resources
- A Survey of Smart Contract Formal Verification - Comprehensive survey of formal verification techniques
- Reentrancy Verification - Reentrancy attack verification using Z3 SMT solver
- SmartScan - Formal verification framework detecting 14 types of vulnerabilities
Contributions are welcome! Please read the contribution guidelines first.
- 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.