Formalizing Correct-by-Construction Casper in Coq

Correct-by-Construction Casper (CBC Casper) is an Ethereum candidate consensus protocol undergoing active design and development. We present a formalization of CBC Casper using the Coq proof assistant that includes a model of the consensus protocol and proofs of safety and non-triviality protocol properties. We leverage Coq's type classes to model CBC Casper at various levels of abstraction. In doing so, we 1) illuminate the assumptions that each protocol property depends on, and 2) reformulate the protocol in general, mathematical terms. We highlight two advantages of our approach: 1) from a proof engineering perspective, it enables a clean separation of concerns between theory and implementation; 2) from a protocol engineering perspective, it provides a rigorous, foundational understanding of the protocol conducive to finding and proving stronger properties. We detail one such new property: strong non-triviality.