Formal Verification of Ethereum 2.0 Deposit Contract
This directory contains the intermediate result of our (ongoing) formal verification of the deposit contract.
Mechanized specifications and proofs in K:
- deposit.k: Formal model of the incremental Merkle tree algorithm
- deposit-spec.k: Correctness specifications
- deposit-symbolic.k: Lemmas (trusted)
To prove the specifications:
- Install K: https://github.com/kframework/k/releases