In ongoing work, we are formally verifying Casper in Coq, both at the
abstract protocol level and at the level of a distributed blockchain
system. In the terminology of Appel et al., we aim to make the Casper
specification two-sided: implementable in Ethereum nodes and provably
beneficial to Ethereum users. A further goal is to lay the foundation
for making the Casper specification live, i.e., enable verifying
Ethereum node implementations. We give some background on Casper and
previous verification efforts, and then describe our modeling and
verification approach.