Formal Methods: Towards a Verified Model of the Algorand Consensus Protocol in Coq

This paper explores the authors' work to model and formally verify the Algorand consensus protocol, proving its security. They note, "two different blocks cannot be certified in the same round, even when the adversary has complete control of message delivery in the network. We believe that our model is sufficiently general and other relevant properties of the protocol such as liveness can be proved for the same model."

To read in full, click here.