Formal Verification of the Ethereum 2.0 Beacon Chain

TL;DR

This paper details the formal verification of the Ethereum 2.0 Beacon Chain's reference implementation, ensuring its correctness and uncovering issues using Dafny to prevent critical bugs in the network.

Contribution

It presents the first formal verification of a major part of the Ethereum 2.0 Beacon Chain implementation, identifying issues and providing verified fixes.

Findings

Uncovered several critical issues in the implementation.

Verified absence of runtime errors in key components.

Developed functional correctness specifications for the Beacon Chain.

Abstract

We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the validators, their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain's network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed verified fixes. We have also synthesised functional correctness specifications that enable us to provide guarantees beyond runtime errors. Our software artefact is available at https://github.com/ConsenSys/eth2.0-dafny.