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 algorithmbytecode-verification/: Bytecode verification of the deposit contract