Formal Verification of the Incremental Merkle Tree Algorithm in Dafny (Eth 2 Deposit Contract)

Eth2 Deposit Contract:Verification of the Incremental Merkle Tree Alg with Dafny · 26 May 2021 · 1:16:05

Franck Cassez describes how he formally verified the Incremental Merkle Tree Algorithm used in the Eth2 deposit contract, using the Dafny verification language. A concrete example of formal verification applied to a core piece of Ethereum infrastructure.

Speakers

• Franck Cassez

Topics

• Security
• Formal Verification
• Developers

From Eth2 Deposit Contract:Verification of the Incremental Merkle Tree Alg with Dafny, hosted by Ethereum Engineering Group.