Ethereum Formal Verification

This page tries to give an overview of the formal verification 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.

Compilers

Solidity

• Yul-Semantics: Yul is an IR language used by the Solidity compiler that provides several different optimizers. Yul formal semantics enables equivalence checking between nonoptimized and optimized versions of the same program.

Ethereum 2.0

Phase 0

• Deposit Contract (Runtime Verification)

Smart Contracts

Projects / Tools

There are several projects aiming at formal 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.

EVM Bytecode

• 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.
• KEVM: K Semantics of the Ethereum Virtual Machine (EVM).
  • Talk: KEVM Overview.
• 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.
• SmartCheck: Static analysis tool for discovering vulnerabilities in Solidity contracts.
  • Paper: SmartCheck: static analysis of ethereum smart contracts, Sergei Tikhomirov et al. (2018).
• Solidity's SMTChecker: SMT-based model checker built-in the Solidity compiler which statically checks safety properties at compile-time, considering an unbounded number of transactions.
  • Talk: Using Solidity's SMTChecker - Devcon IV, Leonardo Alt.
  • Slides: Fully Automated Inductive Invariants Inference for Solidity Smart Contracts - Devcon V, Leonardo Alt.
  • Article: Formal Verification in Solidity, Leonardo Alt.
  • Article: SMTChecker Toward Completeness, Leonardo Alt.
  • 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).

Vyper

• FVyper: A collection of useful Vyper contracts developed with formal methods (KEVM).
• KVyper: Semantics of Vyper in K.

Papers without project pages

• Debugging Smart Contract's Business Logic Using Symbolic Model-Checking, Evgeniy Shishkin (2018).
• Computing Exact Worst-Case Gas Consumption for Smart Contracts, Matteo Marescotti et al. (2018).
• Towards Verification of Ethereum Smart Contracts: A Formalization of Core of Solidity, Jakub Zakrzewski (2018).
• Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts, Shelly Grossman et al. (2018).
• ZEUS: Analyzing Safety of Smart Contracts, Sukrit Kalra et al. (2018).
• Formal Verification of Smart Contracts, Karthikeyan Bhargavan et al. (2016).