Formally Verifying Finality in Gasper: The Core of the Beacon Chain

less than 1 minute read


Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. This post highlights our achievements in formally proving key correctness properties of finality in Gasper using the Coq proof assistant.

Read the article here (also on Medium).