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
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
