Formal Verification of Beacon Chain Specification

This repository consists of the following developments:

1. Mechanized proofs of key properties of finality in the "Gasper" protocol:

   • Model and proofs (in Coq): casper/coq/
   • A technical report describing the model and the proofs: casper/report/

2. (ongoing) Mechanized proofs of the refinement soundness of the state transition (Phase 0) w.r.t. the Gasper protocol:

   • Model (in K): dynamic/dynamic-abstract-beacon-chain.md
   • Proofs (in K): *-spec.k files in dynamic/

3. Analysis on the weak subjectivity period for Ethereum 2.0:

   • Report: [PDF] [Source]

4. Preliminary analysis on the fork choice rule for the Beacon chain:

   • Report: [PDF] [Source]