A Formal Model in K of the Beacon Chain: Ethereum 2.0’s Primary Proof-of-Stake Blockchain

Musab A. Alturki, Denis Bogdanas, Chris Hathhorn and Daejun Park

With the upcoming major update to version 2.0 (code-named Serenity), Ethereum is transitioning into a sharded, proof-of-stake (PoS) consensus mechanism. It brings better energy-efficiency, security and scalability. The specific PoS protocol of Ethereum 2.0 is known as the Beacon Chain.

We are happy to report the first milestone in an ongoing collaboration between Runtime Verification and Ethereum Foundation, to build a formal framework for modeling and verifying the Beacon Chain. We have completed the executable formal model of Beacon Chain in the K Framework. The K specification, along with the technical report describing this work, are both available online.

So what’s the Beacon Chain? How was its model in K developed? Why is this development important?

Continue reading