Runtime Verification Formally Verifies the Algorand Blockchain Will Never Fork

At Algorand, we have an intense focus on security and take every measure possible to ensure that our blockchain is secure. This includes extensive testing, code reviews, and open-sourcing of the code so that everyone can examine it for themselves.

Because code is only as secure as the protocol it implements, we have carefully analyzed and reasoned about the correctness of the Algorand protocol. But we also know that protocols for distributed systems are notoriously difficult to get right, especially protocols that run on unsecured systems and allow anyone to participate without requiring permission from any authority.

To achieve even greater assurance about the Algorand protocol, and to make future design and validation of new protocols easier, we have chosen to enhance our mathematical proofs on paper with machine-checkable formal verification approaches. For this purpose, we engaged Runtime Verification, a company with deep verification expertise, to verify the correctness of the Algorand consensus protocol. We are pleased to report a major milestone in this effort: Using the Coq theorem prover, the team has developed a precise mathematical model of the protocol and formally verified its safety guarantee (that the blockchain never forks). They have written a blog post describing this effort with links to the repository containing the model and the proof. We want to thank Grigore Rosu, Musab A. Alturki, Brandon Moore, Karl Palmskog, and Lucas Pena for their great effort and achievement.