[DEPRECATED: The result in this directory is outdated. The deposit contract has been reimplemented in Solidity and reverified. The latest result can be found at https://github.com/runtimeverification/deposit-contract-verification.]
End-to-End Formal Verification of Ethereum 2.0 Deposit Contract (Vyper Implementation)
This directory provides the result of our end-to-end formal verification of the Ethereum 2.0 deposit contract.
- Final report:
- Blog post: https://runtimeverification.com/blog/end-to-end-formal-verification-of-ethereum-2-0-deposit-smart-contract/
algorithm-correctness/: Formalization and correctness proof of incremental Merkle tree algorithm
bytecode-verification/: Bytecode verification of the deposit contract