Verification of Casper in the Coq Proof Assistant

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