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 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.
- Yul-K: The semantics of the IR Yul formalized in the K framework.
- Yul-Isabelle. The semantics of the IR Yul formalized in Isabelle.
- 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.
- Fully Mechanised Proof of the Deposit Contract's Incremental Merkle tree algorithm in Dafny.
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.
- 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.
- Talk: Smart contracts as inductive systems, Martin Lundfall.
- Scribble: Scribble is a runtime verification tool for Solidity that transforms annotations in the Scribble specification language into concrete assertions that check the specification.
- 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.
- 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.
- 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).
- Certora
- Paper: Finding Bugs Automatically in Smart Contracts with Parameterized Invariants, Thomas Bernardi et al (2020)
- Slither: Solidity static analysis framework that checks for specific vulnerabilities.
- 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.
- 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.