Algorand Official: Runtime Verification officially verifies that the Algorand blockchain never forks

On June 25th, the official Algorand blog post stated that in order to better guarantee the Algorand protocol and make future protocol design and verification easier, Algorand chose to enhance mathematical proof by machine verification. Algorand announced that it has completed the first part of the work, namely the protocol modeling and proof of its safety theorem. Specifically, we used a proof assistant (Coq) to systematically determine the assumption that the protocol is mathematically guaranteed not to fork.