Verification of Casper in the Coq Proof Assistant
Karl Palmskog, Milos Gligoric, Lucas Peña, Brandon M. Moore, Grigore Roşu · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2018
This report describes our effort to model and verify the Casper blockchain finality system in the Coq proof assistant. We outline the salient details on blockchain systems using Casper, describe previous verification efforts we used as a starting point, and give an overview of the formal definitions and properties proved. The Coq source files are available at: https://github.com/runtimeverification/casper-proofs