Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol

TL;DR

This paper formally verifies the safety of Supra's Pipelined Moonshot consensus protocol, ensuring it prevents forks and double spending in blockchain systems with Byzantine validators.

Contribution

It provides the first formal safety proof for Pipelined Moonshot using IVy, extending verification to all network sizes under Byzantine fault assumptions.

Findings

Pipelined Moonshot is fork-free with less than one-third Byzantine validators.

The formal proof guarantees double spending cannot occur due to forks.

The IVy model and proof are publicly available on Github.

Abstract

Decentralized Finance (DeFi) has emerged as a contemporary competitive as well as complementary to traditional centralized finance systems. As of 23rd January 2024, per Defillama approximately USD 55 billion is the total value locked on the DeFi applications on all blockchains put together. A Byzantine Fault Tolerant (BFT) State Machine Replication (SMR) protocol, popularly known as the consensus protocol, is the central component of a blockchain. If forks are possible in a consensus protocol, they can be misused to carry out double spending attacks and can be catastrophic given high volumes of finance that are transacted on blockchains. Formal verification of the safety of consensus protocols is the golden standard for guaranteeing that forks are not possible. However, it is considered complex and challenging to do. This is reflected by the fact that not many complex consensus protocols are formally verified except for Tendermint and QBFT. We focus on Supra's Pipelined Moonshot consensus protocol. Similar to Tendermint's formal verification, we too model Pipelined Moonshot using IVy and formally prove that for all network sizes, as long as the number of Byzantine validators is less than one thirds, the protocol does not allow forks, thus proving that Pipelined Moonshot is safe and double spending cannot be done using forks. The IVy model and proof of safety is available on Github.