Redbelly Network's Use of Formal Verification

Redbelly Network has successfully become one of the first blockchains to employ formal verification to ensure the robustness of its layer 1 consensus protocol.

Redbelly Network's Use of Formal Verification


Redbelly Network is a revolutionary open finance platform that embeds distributed ledger technology into the heart of financial relationships. With a novel leaderless consensus mechanism, democratic byzantine fault tolerant (DBFT) consensus developed with The University of Sydney and CSIRO’s Data61, they are able to achieve high performance, guarantee the impossibility of forking and mitigate double spending with near-instant finality.

Leading up to their launch, Redbelly Network has become the first layer 1 blockchain to use formal verification to test and prove the security and theory behind their consensus protocol.


What is Formal Verification?

Formal verification is a powerful technique used to ensure the correctness and security of blockchain code by applying rigorous mathematical methods to verify that a proof is mathematically correct. It involves creating a formal model of the system, which is then checked against predefined properties and requirements. This approach helps developers identify and eliminate bugs, vulnerabilities, and potential attack vectors before deploying the blockchain code. As the blockchain industry grows, formal verification will become increasingly important in maintaining the trustworthiness and reliability of these systems, setting a higher standard for security and paving the way for more robust blockchain solutions.

How did Redbelly Network use Formal Verification? 

The DBFT Consensus, at the heart of Redbelly Network, was formally verified at the ACM Symposium on Principles of Distributed Computing (PODC) in Salerno, Italy in July 2022. This displays the interest of the scientific community in reducing the human errors in distributed algorithms at the heart of blockchain technologies through the use of machine checked proofs. This also consisted of replacing the partial synchrony assumption with a fairness assumption, which aimed to prove termination. A parameterized model was used to prove that all executions solve the consensus problem regardless of the size of the system and the coalition of hackers.

What does this mean?

The result of this formal verification is that Redbelly Network has positioned itself to offer a verifiably safe and predictable layer 1 blockchain that is appropriate for its use case, to facilities the onboarding and management of real world assets and existing financial relationships on chain.

Redbelly Network is setting the standard for the security and verification measures that an industry leading blockchain must undergo.

Learn more about Redbelly Network and its use of Formal Verification

To learn more about Redbelly Network and its use of formal verification, visit their blog here

“Security is not a product, but a process." – Bruce Schneier


Redbelly Network is set to launch later this year, and has laid the foundation to be an industry leader for enterprise and financial use cases on the blockchain.

Subscribe to receive articles right in your inbox