  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.
