Verification of the Incremental Merkle Tree Algorithm with Dafny
Franck Cassez
TL;DR
This paper presents a formally verified implementation and correctness proof of the incremental Merkle tree algorithm used in Ethereum 2.0's Deposit Smart Contract, ensuring its reliability through machine-checkable proofs.
Contribution
It provides the first machine-checkable version and correctness proof of the incremental Merkle tree algorithm with verified optimizations.
Findings
First Dafny-based correctness proof of the algorithm
Complete machine-checkable Dafny code base provided
Verified optimizations of the algorithm included
Abstract
The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsBlockchain Technology Applications and Security · Distributed systems and fault tolerance · Security and Verification in Computing