@inproceedings{a4a2b88c11774ce5984c38d4dd6368ee,
title = "Formalizing Correct-by-Construction Casper in Coq",
abstract = "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.",
keywords = "Coq, Ethereum, blockchain, consensus protocols, formal verification",
author = "Elaine Li and Traian Serbanuta and Denisa Diaconescu and Vlad Zamfir and Grigore Rosu",
note = "Publisher Copyright: {\textcopyright} 2020 IEEE.; 2nd IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020 ; Conference date: 02-05-2020 Through 06-05-2020",
year = "2020",
month = may,
doi = "10.1109/ICBC48266.2020.9169468",
language = "English (US)",
series = "IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
booktitle = "IEEE International Conference on Blockchain and Cryptocurrency, ICBC 2020",
address = "United States",
}