Ethereum Formal Verification

This page tries to give an overview of the formal verification (and related) projects in the Ethereum ecosystem, extending and updating https://github.com/pirapira/ethereum-formal-verification-overview.

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

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

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

You might also want to visit the Ethereum Formal Methods Gitter channel.

Compilers

Solidity / Yul

• Yul-ACL2. The semantics of the IR Yul formalized in ACL2 framework.
• Yul-Isabelle. The semantics of the IR Yul formalized in Isabelle.
• 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-K: The semantics of the IR Yul formalized in the K framework.
• Solidity Optimizer Transformations. Formalizes in ACL2 and verifies correctness of some of the Yul optimizer transformations present in the Solidity compiler.

Ethereum 2.0

Phase 0

• Deposit Contract (Runtime Verification) (part 1)
• Deposit Contract (Runtime Verification) (part 2)
• Formal Verification of the Eth2.0 Specs in Dafny: The objective of this project is to write a formal specification of the Eth2.0 specification in the verification-aware programming language Dafny.
  • 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.

Smart Contracts

Projects / Tools

There are several projects aiming at formal specification and verification of smart contracts. The list given here is separated by target language and then sorted alphabetically. A few resource links are given with each project. For more resources on a specific project 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 https://ntu-srslab.github.io/smart-contract-publications/ and type 2020 into the search box. For that reason I am not listing anymore 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.

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 Specification Language: Used by the Certora verification tool 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.

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.
  • 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

EVM Bytecode

• Certora
  • Paper: Finding Bugs Automatically in Smart Contracts with Parameterized Invariants, Thomas Bernardi et al (2020)
• EthBMC: A Bounded Model Checker for Smart Contracts.
• 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.
  • Talk: Formal Verification of Smart Contracts, Yoichi Hirai.
• eThor: Static analysis for Ethereum smart contracts.
• 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. To appear.
  • Paper: Super-Optimization of Smart Contracts. Elvira Albert, Pablo Gordillo, Alejandro Hernández-Cerezo, Albert Rubio and Maria A. Schett, 2022. To appear.
• 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.
• 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).
• KLab: K framework proof explorer and smart contract specification format.
  • Tutorial: KLab, Everett Hildenbrandt.
  • Workshop: Formal Verification Workshop Using KLab - Devcon IV. Could not find video/slides.
• 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.
  • 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.
• Oyente: EVM bytecode analysis tool based on symbolic execution.
  • Paper: Making Smart Contracts Smarter, Loi Luu et al. (2016).
• Securify: Security scanner for Ethereum smart contracts.
  • Paper: Securify: Practical Security Analysis of Smart Contracts, Petar Tsankov et al. (2018).
• VerX: Full functional verification for Ethereum smart contracts.
  • Paper: VerX: Safety Verification of Smart Contracts, Permenev et al. (2019).

Solidity

• 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.
  • 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.
  • Paper: SmartCheck: static analysis of ethereum smart contracts, Sergei Tikhomirov et al. (2018).
• Solidifier: Bounded Model Checker for Solidity.
• 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.
  • 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 verified for Solidity smart contracts, based on automatic inference of contract invariants.
• VeriSol: Formal specification, verification and scalable refutation of Solidity smart contracts using code contracts, Boogie and Corral.
  • 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.

Vyper

• 2vyper: Automatic verifier for Vyper smart contracts, based on the Viper verification infrastructure.
• FVyper: A collection of useful Vyper contracts developed with formal methods (KEVM).
• KVyper: Semantics of Vyper in K.

Arithmetic Circuits and Zero Knowledge Applications

• 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.
• Ecne: An engine for verifying the soundness of R1CS constraints.
• Leo
  • Paper: LEO: A Programming Language for Formally Verified, Zero-Knowledge Applications

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