Blog Posts

2020

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.

2019

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.