Formally Modeling Algorand and Verifying its Safety Property

less than 1 minute read


I posted an article celebrating the successful completion of the first part of an ongoing collaboration between Runtime Verification and Algorand, to model Algorand’s consensus protocol and verify its safety theorem using the Coq proof assistant].

Read the article here (also on Medium).