Ethereum Formal Verification

This page gives an overview of the formal verification (and related analysis) projects in the Ethereum ecosystem. It extends and updates pirapira/ethereum-formal-verification-overview.

The focus is formal verification and other types of analysis of smart contracts, while also gathering information about formal verification of protocols and compilers.

The lists are not complete, and you are encouraged to visit the project pages to learn more about them.

Please do not hesitate to open an issue/PR if you have information that is not present here or if you find a mistake.

Maintenance status: entries marked ⚠️ are archived or have had no commits in over a year (as of June 2026). They are kept for historical reference; an inactive project may still be perfectly usable.

Contents

• Smart Contracts
  • Learning
  • Specification
  • Fuzzing
  • Economics / Game Theory
  • EVM Bytecode
  • Solidity
  • Vyper
• Compilers & Intermediate Languages
• Ethereum Protocol
• Zero-Knowledge Applications & Arithmetic Circuits
• Other Lists

Smart Contracts

There are several projects aiming at formal specification and verification of smart contracts. The list below is separated by target language / technique and then sorted alphabetically. A few resource links are given with each project; for more, please visit the project's page.

There is also an overwhelming amount of papers describing techniques related to formal verification of smart contracts. For example, visit ntu-srslab/smart-contract-publications and type 2020 into the search box. For that reason I am not listing any more papers describing techniques for which I could not find the actual tool.

Learning

• Formal Methods for DeFi Developers: a course sequence for training developers in the use & development of formal methods and formal tools. ⚠️ No commits since 2022-07.

Specification

• Act: Act allows specification of storage updates, pre/post conditions and contract invariants. Its tool suite also has proof backends able to prove many properties via Coq, SMT solvers, or hevm.
  • Article: Act 0.1 Release & Tutorial, David Terry.
  • Talk: Smart contracts as inductive systems, Martin Lundfall.
• Certora Verification Language (CVL): Used by the Certora Prover to write properties about analyzed contracts.
• Scribble: Scribble is a runtime verification tool for Solidity that transforms annotations in the Scribble specification language into concrete assertions that check the specification.

Fuzzing

• Echidna: A fast smart contract fuzzer. It is designed for fuzzing and property-based testing.
• Harvey: A fuzzer for Ethereum smart contracts.
• hevm: hevm is many things as you will see below, including a fuzzer. The fuzzer can also be used to try to break invariants.
  • Article: Symbolic Execution With ds-test, David Terry.
• ItyFuzz: Snapshot-based hybrid fuzzer for EVM (and MoveVM) bytecode that combines fuzzing with symbolic execution to reach deep states quickly.
  • Paper: ItyFuzz: Snapshot-Based Fuzzer for Smart Contract, Chaofan Shou, Shangyin Tan, Koushik Sen (ISSTA 2023).

Economics / Game Theory

• Clockwork Finance Framework: A general purpose formal verification framework and mechanized proof system for reasoning about economic security properties of composed DeFi contracts, using K framework's symbolic execution engine and model checker. ⚠️ No commits since 2021-09.
  • Paper: Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts
  • Talk: Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts - SBC22
  • Slides: Clockwork Finance
• CheckMate: A framework designed to automatically check game-theoretic security properties of games modeling blockchain/off-chain protocols.
  • Paper: Divide and Conquer: a Compositional Approach to Game-Theoretic Security (OOPSLA25)
  • Paper on modelling protocols as games: Game Modeling of Blockchain Protocols (iFM25)

EVM Bytecode

• Blanc: An EVM programming language in Lean 4 with compiler-correctness and WETH solvency proofs.
• Certora
  • Paper: Finding Bugs Automatically in Smart Contracts with Parameterized Invariants, Thomas Bernardi et al (2020)
• EquiVM: Refinement proofs in Lean 4 that EVM bytecode implements a high-level program written in Sol⁻, a Solidity-like specification language, intended to be produced by LLM agents.
• EthBMC: A Bounded Model Checker for Smart Contracts. ⚠️ No commits since 2022-12.
• EtherTrust: Analysis tool for EVM bytecode.
  • Paper: Foundations and Tools for the Static Analysis of Ethereum smart contracts, Ilya Grishchenko et al. (2018).
• EthIsabelle: A Lem formalization of EVM and some Isabelle/HOL proofs. ⚠️ No commits since 2022-03.
  • Talk: Formal Verification of Smart Contracts, Yoichi Hirai.
• eThor: Static analysis for Ethereum smart contracts.
• EVM-Dafny: A formal and executable semantics of the EVM in Dafny.
  • Paper (FM23): Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny, Franck Cassez et al. (2023).
  • Paper (arXiv version): Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny, Franck Cassez et al. (2023).
• evm-sail: A formal and executable specification of the EVM in Sail, the ISA-specification language behind the official RISC-V model, exporting to Coq, Isabelle/HOL, HOL4 and Lean.
  • Docs: evm-sail documentation and benchmarks.
• EvmSemantics: A relational small-step and big-step semantics of the EVM in Lean 4, with an executable interpreter proven sound against the relation.
• evm-smith: A framework for AI systems to write EVM bytecode and prove it safe, built on EVMYulLean.
• EVMYulLean: An executable formal model of the EVM and the Yul IR in Lean 4.
• GASOL: A generic framework that optimizes smart contracts by applying the technique called "super-optimization" that consists in optimizing basic blocks.
  • Paper: A Max-SMT Superoptimizer for EVM handling Memory and Storage. Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo and Albert Rubio, TACAS 2022.
  • Paper: Super-Optimization of Smart Contracts. Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio and Maria A. Schett, 2022.
• Halmos: Symbolic testing tool (a16z) that symbolically executes Foundry/Solidity tests to prove or refute assertions over all possible inputs.
• hevm: Symbolic execution engine and equivalence checker for EVM code.
  • Article: Symbolic Execution With ds-test, David Terry.
  • Article: Symbolic execution for hevm, Martin Lundfall.
• Jaune: An executable formal specification of the EVM in Lean 4.
• KEVM: K Semantics of the Ethereum Virtual Machine (EVM).
  • Talk: KEVM Overview.
  • Paper: KEVM: A Complete Semantics of the Ethereum Virtual Machine, Everett Hildenbrandt et al. (2017).
• Kontrol: Combines KEVM and Foundry to let developers run K-framework symbolic-execution proofs directly from their Solidity test suites.
• Manticore: EVM bytecode analysis tool based on symbolic execution.
  • Article: Manticore: Symbolic execution for humans.
  • Workshop: Using Manticore and Symbolic Execution to Find Smart Contracts Bugs - Devcon IV.
• MAIAN: EVM bytecode analysis tool that checks whether a contract might be suicidal, prodigal or greedy. ⚠️ No commits since 2023-10.
  • Paper: Finding The Greedy, Prodigal, and Suicidal Contracts at Scale, Ivica Nikolic et al. (2018).
• Mythril: EVM bytecode security analysis tool that uses concolic analysis, taint analysis and control flow checking.
  • Article: Practical Smart Contract Security Analysis and Exploitation— Part 1, Bernhard Mueller.
• Securify: Security scanner for Ethereum smart contracts. ⚠️ No commits since 2025-05.
  • Paper: Securify: Practical Security Analysis of Smart Contracts, Petar Tsankov et al. (2018).
• Verifereum: Specification of the EVM and full functional verification of EVM bytecode in HOL4.
• VerX: Full functional verification for Ethereum smart contracts.
  • Paper: VerX: Safety Verification of Smart Contracts, Permenev et al. (2019).
• KLab: K framework proof explorer and smart contract specification format. ⚠️ Archived; no commits since 2021-08.
  • Tutorial: KLab, Everett Hildenbrandt.
  • Workshop: Formal Verification Workshop Using KLab - Devcon IV. Could not find video/slides.
• Oyente: EVM bytecode analysis tool based on symbolic execution. ⚠️ Archived; no commits since 2023-01.
  • Paper: Making Smart Contracts Smarter, Loi Luu et al. (2016).

Solidity

• Clear: Interactive formal-verification framework for Yul/Solidity programs, built on Nethermind's Lean model of the Yul EVM dialect.
• Pyrometer: Combines abstract interpretation, symbolic execution, and static analysis to perform value-range and reachability (bound) analysis on Solidity. ⚠️ No commits since 2025-02.
• Slither: Solidity static analysis framework that checks for specific vulnerabilities.
  • Article: Slither – a Solidity static analysis framework.
• SmartAce: An automated framework for smart contract verification. ⚠️ No commits since 2022-01.
  • Paper: Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE, Scott Wesley et al. (2022).
• SmartCheck: Static analysis tool for discovering vulnerabilities in Solidity contracts. ⚠️ No commits since 2023-05.
  • Paper: SmartCheck: static analysis of ethereum smart contracts, Sergei Tikhomirov et al. (2018).
• Solidifier: Bounded Model Checker for Solidity. ⚠️ No commits since 2020-12.
  • Paper: Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling, Pedro Antonino & A. W. Roscoe (2021).
• Solidity's SMTChecker: SMT and Horn-based model checker built-in the Solidity compiler which statically checks safety properties at compile-time, considering an unbounded number of transactions.
  • Slides: Formally Verifying Ethereum Smart Contracts by Overwhelming Horn Solvers, Dagstuhl Seminar on Rigorous Methods for Smart Contracts, Leonardo Alt.
  • Talk: Fully Automated Formal Verification: How far can we go? - EthCC 4, Leonardo Alt & Martin Lundfall.
  • Slides: Fully Automated Formal Verification: How far can we go? - EthCC 4, Leonardo Alt & Martin Lundfall.
  • Article: Automated Synthesis of External Unknown Functions, Leonardo Alt.
  • Talk: Fully Automated Inductive Invariants Inference for Solidity Smart Contracts - Devcon V, Leonardo Alt.
  • Slides: Fully Automated Inductive Invariants Inference for Solidity Smart Contracts - Devcon V, Leonardo Alt.
  • Article: SMTChecker Toward Completeness, Leonardo Alt.
  • Paper: Accurate Smart Contract Verification through Direct Modelling, Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti E. J. Hyvärinen, and Natasha Sharygina (2020).
  • Paper: SMT-Based Verification of Solidity Smart Contracts, Leonardo Alt and Christian Reitwiessner (2018).
• solc-verify: Functional verification of Solidity code using annotations and modular program verification. ⚠️ No commits since 2023-09.
  • Paper: solc-verify: A Modular Verifier for Solidity Smart Contracts, Á. Hajdu, D. Jovanović (2019).
  • Talk: solc-verify, a source-level formal verification tool for Solidity smart contracts, given by Á. Hajdu at Solidity Summit (2020)
  • Paper: SMT-Friendly Formalization of the Solidity Memory Model, Á. Hajdu, D. Jovanović (2020).
  • Talk: SMT-Friendly Formalization of the Solidity Memory Model, given by Á. Hajdu at SMT (2020)
  • Paper: Formal Specification and Verification of Solidity Contracts with Events, Á. Hajdu, D. Jovanović, G. Ciocarlie (2020).
  • Talk: Formal Specification and Verification of Solidity Contracts with Events, given by Á. Hajdu at FMBC (2020).
• VeriSmart: Safety verifier for Solidity smart contracts, based on automatic inference of contract invariants. ⚠️ No commits since 2023-01.
• VeriSol: Formal specification, verification and scalable refutation of Solidity smart contracts using code contracts, Boogie and Corral. ⚠️ No commits since 2022-12.
  • Slides: Formal Verification of Smart Contracts and Protocols: What, Why, How - Devcon V, Shuvendu Lahiri et al.
  • Article: Researchers work to secure Azure Blockchain smart contracts with formal verification, Microsoft Research Blog.
  • Paper: Formal Specification and Verification of Smart Contracts for Azure Blockchain, Yuepeng Wang, Shuvendu K. Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Born, Immad Naseer.
• Verity: A Lean-based EDSL to specify, implement, and prove Ethereum smart contracts, compiling verified contracts down to EVM bytecode with machine-checked spec/implementation equivalence. (veritylang.com)
• Wake: Python framework combining a Solidity static-analysis detector framework, property-based fuzzing, and developer tooling.

Vyper

• Vyper-HOL: Semantics of Vyper and verified compilation of Vyper in HOL4.
• 2vyper: Automatic verifier for Vyper smart contracts, based on the Viper verification infrastructure. ⚠️ No commits since 2023-02.
• FVyper: A collection of useful Vyper contracts developed with formal methods (KEVM). ⚠️ Archived; no commits since 2021-04.
• KVyper: Semantics of Vyper in K. ⚠️ No commits since 2018-08.

Compilers & Intermediate Languages

Solidity / Yul

• Yul-ACL2. The semantics of the IR Yul formalized in the ACL2 framework.
• yul-compiler: A verified compiler from a fragment of Yul to EVM bytecode in Lean 4, proven correct against yul-semantics and EvmSemantics, rejecting what it cannot verify rather than emitting unverified code.
• Yul-Isabelle. The semantics of the IR Yul formalized in Isabelle. ⚠️ No commits since 2022-11.
• Yul-Lean: A formal specification of the Yul IR semantics in the Lean proof assistant.
  • Article: Securing Warp: A formal specification of the Yul IR, Julian Sutherland.
• yul-semantics: A gas-free big-step relational semantics of Yul in Lean 4, parameterized over an abstract dialect, with an executable interpreter proven adequate.
• Solidity Optimizer Transformations. Formalizes in ACL2 and verifies correctness of some of the Yul optimizer transformations present in the Solidity compiler.
• Yul-K: The semantics of the IR Yul formalized in the K framework. ⚠️ Archived; no commits since 2019-10.

Ethereum Protocol

Consensus Layer

Formerly labelled "Eth2" / "Ethereum 2.0" (the Beacon Chain and its "Phase 0" rollout). The Eth1/Eth2 terminology has since been deprecated in favor of "execution layer" and "consensus layer".

• SizzLean: A Lean 4 implementation of SSZ, the serialization and Merkleization format of the Ethereum consensus layer, with roundtrip, non-malleability, and size-bound theorems proved for the fixed-size types and full conformance against the upstream consensus-spec-tests.
• Deposit Contract (Runtime Verification): end-to-end formal verification of the Eth2 deposit contract.
  • Part 1
  • Part 2
• Formal Verification of the Eth2.0 Specs in Dafny: A formal specification of the Eth2.0 specification in the verification-aware programming language Dafny. ⚠️ Archived; no commits since 2024-06.
  • Paper: Formal Verification of the Ethereum 2.0 Beacon Chain, Franck Cassez, Joanne Fuller, Aditya Asgaonkar.
• Fully Mechanised Proof of the Deposit Contract's Incremental Merkle tree algorithm in Dafny. ⚠️ Archived; no commits since 2021-09.

Zero-Knowledge Applications & Arithmetic Circuits

• ACL2 formalization of Semaphore
  • Semaphore
  • ACL2 Semaphore Docs
• Cairo verification using Lean
  • Paper: A verified algebraic representation of Cairo program execution, Jeremy Avigad et al.
• circomspect: Trail of Bits static analyzer/linter for Circom circuits, with multiple passes that flag under-constrained signals and other circuit bugs. ⚠️ No commits since 2024-06.
• circuzz: Metamorphic and differential fuzzing pipeline for zero-knowledge circuit compiler toolchains.
• CIVER: Modular verifier of weak safety (absence of under-constrained signals), tag specifications, and pre/postconditions for Circom circuits.
• Coda: A statically-typed language for ZK circuits with a refinement type system that discharges proof obligations to Coq.
• Ecne: An engine for verifying the soundness of R1CS constraints. ⚠️ No commits since 2022-08.
• gnark-lean-extractor: Extracts gnark (zk-SNARK library) circuits defined in Go into Lean for formal verification. ⚠️ No commits since 2025-04.
• Korrekt (halo2-analyzer): Uses abstract interpretation and SMT to detect under-constrained cells and unused gates/columns in Halo2 (PLONKish) circuits.
• Leo
  • Paper: LEO: A Programming Language for Formally Verified, Zero-Knowledge Applications
• Picus: Automated verifier (Veridise) for the uniqueness / under-constrained property of ZKP circuits (Circom, R1CS, gnark), using SMT solvers. ⚠️ No commits since 2024-03 (an actively maintained fork lives at chyanju/Picus).
• Verified zk(E)VM: A research effort accelerating the application of formal verification to zk(E)VMs in Lean (verified-zkevm.org).
  • ArkLib: Formally verified arguments of knowledge in Lean.
  • clean: A verified Lean circuit DSL.
  • evm-asm: An experimental verified macro assembler in Lean 4 over a RISC-V RV64IM backend, targeting a zkEVM stateless block validator with no compiler in the trusted computing base.
• zkFuzz: Program-mutation fuzzing framework for ZK circuits, formalizing a Trace-Constraint Consistency Test to find under/over-constraint bugs.

Other Lists

• Crytic Awesome Ethereum Security: Less focused on formal verification but has a broader scope of types of tools.
• Consensys Security Best Practices: Best practices and list of security tools.
• ethereum.org: Intro to security of smart contracts.
• OpenZeppelin's list of Post-Mortems