2020-06-10

End-to-End Formal Verification of Ethereum 2.0 Deposit Contract

This provides the artifact of our end-to-end formal verification of the Ethereum 2.0 deposit contract written in Solidity.

[NOTE: The deposit contract had initially been written in Vyper, but later it was reimplemented in Solidity. The formal verification of the initial Vyper implementation can be found at here].

Documents:

• Final report: deposit-contract-verification.pdf
• Blog posts:
  • Formal Verification of Ethereum 2.0 Deposit Contract (Part I) (June 12, 2019)
  • End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract (January 20, 2020)

Verification artifacts:

• algorithm-correctness/: Formalization and correctness proof of incremental Merkle tree algorithm
• bytecode-verification/: Bytecode verification of the deposit contract

Resources

Disclaimer

License