Runtime Verification Formally Verifies the Algorand Blockchain Will Never Fork

Algorand
Algorand
Jun 25, 2019 · 2 min read
Image for post
Image for post

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.

Algorand

Algorand Inc.

Algorand

Written by

Algorand

A scalable, secure and decentralized digital currency and transactions platform.

Algorand

Algorand

Algorand Inc. built the world’s first open source, permissionless, pure proof-of-stake blockchain protocol for the next generation of financial products. This blockchain, the Algorand protocol, is the brainchild of Turing Award-winning cryptographer Silvio Micali.

Algorand

Written by

Algorand

A scalable, secure and decentralized digital currency and transactions platform.

Algorand

Algorand

Algorand Inc. built the world’s first open source, permissionless, pure proof-of-stake blockchain protocol for the next generation of financial products. This blockchain, the Algorand protocol, is the brainchild of Turing Award-winning cryptographer Silvio Micali.

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store