Skip to content

Latest commit

 

History

History
87 lines (63 loc) · 7.51 KB

File metadata and controls

87 lines (63 loc) · 7.51 KB

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

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

Solidity

Vyper

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

Papers without project pages