Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

Formally Verifying Finality in Gasper: The Core of the Beacon Chain

less than 1 minute read

Published:

Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. This post highlights our achievements in formally proving key correctness properties of finality in Gasper using the Coq proof assistant.

K vs. Coq as Language Verification Frameworks

less than 1 minute read

Published:

Ever wondered how K and Coq compare and contrast as language verification frameworks? I posted a series of articles comparing K and Coq as language verification frameworks through a working example.

projects

publications

talks

teaching