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.

翻译：去中心化金融（DeFi）已成为传统中心化金融体系的当代竞争者与补充者。截至2024年1月23日，据Defillama数据，所有区块链上DeFi应用锁定的总价值约为550亿美元。拜占庭容错（BFT）状态机复制（SMR）协议，通常称为共识协议，是区块链的核心组件。若共识协议中存在分叉可能，则可能被滥用于实施双花攻击，鉴于区块链上交易的高额金融价值，这将是灾难性的。共识协议安全性的形式化验证是保证不可分叉的黄金标准，但通常被认为复杂且具有挑战性。这一点体现在除Tendermint和QBFT外，鲜有复杂共识协议通过形式化验证。我们聚焦于Supra的流水线Moonshot共识协议。与Tendermint的形式化验证类似，我们同样使用IVy对流水线Moonshot建模，并形式化证明：对于所有网络规模，只要拜占庭验证者数量少于三分之一，该协议便不允许分叉，从而证明流水线Moonshot是安全的，且无法利用分叉实施双花攻击。IVy模型及安全性证明已发布于Github。