Blockchain systems such as Ethereum are increasingly used as financial transaction mechanisms (cryptocurrencies). However, in a blockchain system, there may be several competing chains of blocks (forks) that only agree on the transaction history up to some point, potentially leading to some transactions being dropped. To address the problem of blockchain revisions, Buterin and Griffith proposed a blockchain finality system overlay called Casper. When enough participants are honest, Casper defends both against active attacks and catastrophic crashes. 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. We build directly on two previous modeling and verification efforts: verified abstract models of Casper in Isabelle/HOL, and a model in Coq of a general distributed blockchain system called Toychain. Our verification approach bridges these two efforts by translating Isabelle/HOL definitions and proofs to Coq and specializing Toychain definitions for Casper. We give an overview of our ongoing verification effort and outline how we encode and prove key Casper properties, such as accountable safety, which rules out agreement on conflicting blocks when less than one third of participants behave adversarially.