Overview of the formal verification projects in the Ethereum ecosystem.
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
LICENSE
README.md

README.md

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.

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