Threshold cryptography is essential for many blockchain protocols. For example, many protocols rely on threshold common coin to implement asynchronous consensus, leader elections, and provide support for randomized applications. Similarly, threshold decryption and threshold time-lock puzzles are often necessary for privacy. In this paper, we study the interplay between threshold cryptography and a class of blockchains that use Byzantine-fault tolerant (BFT) consensus protocols with a focus on latency. More specifically, we focus on blockchain-native threshold cryptosystem, where the blockchain validators seek to run a threshold cryptographic protocol once for every block with the block contents as an input to the threshold cryptographic protocol. All existing approaches for blockchain-native threshold cryptosystems introduce a latency overhead of at least one message delay for running the threshold cryptographic protocol. In this paper, we first propose a mechanism to eliminate this overhead for blockchain-native threshold cryptosystems with tight thresholds, i.e., in threshold cryptographic protocols where the secrecy and reconstruction thresholds are the same. However, many real-world proof-of-stake-based blockchain-native threshold cryptosystems rely on ramp thresholds, where reconstruction thresholds are strictly greater than secrecy thresholds. For these blockchains, we formally demonstrate that the additional delay is unavoidable. We then introduce a mechanism to minimize this delay in the optimistic case. We implement our optimistic protocol for the proof-of-stake distributed randomness scheme on the Aptos blockchain. Our measurements from the Aptos mainnet show that the optimistic approach reduces latency overhead by 71%.
The process of reaching an agreement on a value within a distributed network, known as a consensus problem, is a defining feature of blockchain. This consensus problem can be seen in various applications like load balancing, transaction validation in blockchain, and distributed computing. In recent years, many researchers have provided solutions to this problem. Hence we have presented a survey in which we delved into blockchain consensus algorithms and conducted a comparative analysis of all the consensus algorithms to provide information about each protocol’s advantages and drawbacks. This survey starts with the standard proof-of-work consensus protocol applied in bitcoin cryptocurrency and its limitations on the ground of the following parameters: throughput (transactions per second), latency, forks, fault tolerance, double spending attacks, and power consumption. The rest of the consensus algorithms in this paper have been systematically covered to address the limitations of proof-of-work. This paper also covered Raft and PBFT consensus algorithms suitable for permissioned networks. Although the PBFT consensus protocol has a high throughput and a low latency, it has limited node scalability. The PBFT has a low byzantine fault tolerant rate. This paper also covers PoEWAL for blockchain-based IoT applications and WBFT, which prevents corrupt nodes from taking part in consensus. A comparative analysis of the consensus algorithms provides an explicit knowledge of the present research, which also offers guidance for future study.
This study builds on our previous systematic literature review (SLR) that assessed the applications and performance of zk-SNARK, zk-STARK, and Bulletproof non-interactive zero-knowledge proof (NIZKP) protocols. To address the identified research gaps, we designed and implemented a benchmark comparing these three protocols using a dynamic minimized multiplicative complexity (MiMC) hash application. We evaluated performance across four general-purpose programming libraries and two programming languages. Our results show that zk-SNARK produced the smallest proofs, while zk-STARK generated the largest. In terms of proof generation and verification times, zk-STARK was the fastest, and Bulletproof was the slowest. Interestingly, zk-SNARK proofs verified marginally faster than zk-STARK, contrary to other findings. These insights enhance our understanding of the functionality, security, and performance of NIZKP protocols, providing valuable guidance for selecting the most suitable protocol for specific applications.
En el ecosistema de las aplicaciones descentralizadas (DApps), la dependencia de un único nodo de blockchain para realizar todas las transacciones presenta varios desafíos críticos, entre ellos la falta de redundancia y la potencial inestabilidad en caso de fallos en dicho nodo. Este problema subraya la necesidad de un sistema que permita la configuración y monitoreo de múltiples nodos, asegurando una alta disponibilidad y un equilibrio de carga eficiente. El presente Trabajo de Final de Grado, titulado "HIGH AVAILABILITY ETHEREUM-LIKE NODE PROXY", aborda esta problemática proponiendo una solución basada en una aplicación desarrollada en Python para monitorear y equilibrar el tráfico entre varios nodos Ethereum JSON-RPC.
Decentralized Physical Infrastructure Networks (De-PINS) are secured and governed by blockchains but beyond crypto-economic incentives, they lack measures to establish trust in participating devices and their services. The verification of relevant device credentials during device registration helps to overcome this problem. However, on-chain verification in decentralized applications (dApp) discloses potentially confidential device attributes whereas off-chain verification introduces undesirable trust assumptions. In this paper, we propose a credential-based device registration (CDR) mechanism that verifies device credentials on the blockchain and leverages zero-knowledge proofs (ZKP) to protect confidential device attributes from being disclosed. We characterize CDR for DePINs, present a general system model, and technically evaluate CDR using zkSNARKs with Groth16 [1] and Marlin [2]. Our experiments give first insights into performance impacts and reveal a tradeoff between the applied proof systems.
In this paper, we present a decentralized network protocol, Space Network Protocol, based on Communication Satellite Services. The protocol outlines a method for distributing information about the status of satellite communication services across the entire blockchain network, facilitating fairness and transparency in all communication services. Our primary objective is to standardize the services delivered by all satellite networks under the communication satellite protocol. This standard remains intact regardless of potential unreliability associated with the satellites or the terminal hardware. We proposed PoD (Proof of Distribution) to verify if the communication satellites are online and PoF (Proof of Flow) to authenticate the actual data flow provided by the communication satellites. In addition, we also proposed PoM (Proof of Mesh) to verify if the communication satellites have successfully meshed together. Utilizing zero-knowledge proof and multi-party cryptographic computations, we can evaluate the service provisioning parameters of each satellite, even in the presence of potential terminal or network node fraud. This method offers technical support for the modeling of distributed network services.
Jun 17, 2024·Proceedings of the 2024 Workshop on Advanced Tools, Programming Languages, and PLatforms for Implementing and Evaluating algorithms for Distributed systems
Reaching consensus despite faulty or corrupted nodes is a central question in distributed computing; it has received renewed attention over the last years because of its importance for cryptocurrencies and blockchain networks. Modern consensus protocols in this space have relied on a number of different methods for the nodes to influence protocol decisions. Such assumptions include (1) traditional voting, where each node has one vote, (2) weighted voting, where voting power is proportional to stake in an underlying asset, and (3) proof-of-X, which demonstrates a cryptographically verifiable investment of a resource X, such as storage space, time waited, or computational work.
Chris Natoli, Parinya Ekparinya, Guillaume Jourjon, Vincent Gramoli
Traditional blockchain systems offer a secure way of tracking the ownership of digital assets as long as the attacker does not control a large portion of the overall computational or mining power. They typically require participants to generate a proof-of-work before proposing a block at a given index of the chain. To choose one block among the candidate blocks at the same index, Nakamoto’s consensus, Ghost , and the original Ethereum’s consensus select, respectively, the longest branch, the heaviest subtree and the branch with the most difficult crypto-puzzles. This allows an attacker who can generate proofs-of-work faster than others to double spend by overwriting any given branch. In this article, we present a double spending attack, called the Balance attack, that simply needs to delay some messages. This result sheds new lights on an important, often implicit, assumption of the blockchain, synchrony , under which the transmission delay of any message should be within a known upper bound. We show that the attack succeeds with high probability on the protocols of the two largest blockchain systems in market capitalization, Bitcoin and Ethereum. To quantify the impact of our attack, we replicated the blockchain network run by 50 financial institutions and achieved double spending in less than 20 minutes. Finally, we demonstrate the success of the attack empirically by modifying the geth software and hijacking BGP in a controlled distributed system whose distribution of mining power is set to the distribution observed on the Ethereum main blockchain.
David Melo, Saúl E. Pomares Hernández, Lil María Rodríguez-Henríquez, Julio César Pérez-Sansalvador
Blockchain technology ensures record-keeping by redundantly storing and verifying transactions on a distributed network of nodes. Permissionless blockchains have pushed the development of decentralized applications (DApps) characterized by distributed business logic, resilience to centralized failures, and data immutability. However, storage scalability without sacrificing throughput is one of the remaining open challenges in permissionless blockchains. Enhancing throughput often compromises storage, as seen in projects such as Elastico, OmniLedger, and RapidChain. On the other hand, solutions seeking to save storage, such as CUB, Jidar, SASLedger, and SE-Chain, reduce the transactional throughput. To our knowledge, no analysis has been performed that relates storage growth to transactional throughput. In this article, we delve into the execution of the Bitcoin and Ethereum transactional models, unlocking patterns that represent any transaction on the blockchain. We reveal the trade-off between transactional throughput and storage. To achieve this, we introduce the spent-by relation, a new abstraction of the UTXO model that utilizes a directed acyclic graph (DAG) to reveal the patterns and allows for a graph with granular information. We then analyze the transactional patterns to identify the most storage-intensive ones and those that offer greater flexibility in the throughput/storage trade-off. Finally, we present an analytical study showing that the UTXO model is more storage-intensive than the account model but scales better in transactional throughput.
The rapid advancement of technology, alongside state-of-the-art techniques is at an all-time high. However, this unprecedented growth of technological prowess also brings forth potential threats, as oftentimes the security encompassing these technologies is imperfect. Particularly within the automobile industry, the recent strides in technology have brought about increased complexity. A notable flaw lies in the CAN-FD protocol, which lacks robust security measures, making it vulnerable to data theft, injection, replay, and flood data attacks. With the rising complexity of in-vehicular networks and the widespread adoption of CAN-FD, the imperative to safeguard the protocol has never been more crucial. This paper aims to provide a comprehensive review of the existing in-vehicle communication protocol, CAN-FD. It explores existing security approaches designed to fortify CAN-FD, demonstrating multiple multi-layer solutions that leverage modern techniques including Physical Unclonable Function (PUF), Elliptical Curve Cryptography (ECC), Ethereum Blockchain, and Smart contracts. The paper highlights existing multi-layer security measures that offer minimal overhead, optimal performance, and robust security. Moreover, it identifies areas where these security measures fall short and discusses ongoing research along with suggestions for implementing software and hardware-level modifications. These proposed changes aim to streamline complexity, reduce overhead while ensuring forward compatibility. In essence, the methods outlined in this study are poised to excel in real-world applications, offering robust protection for the evolving landscape of in-vehicular communication systems.
Mayank Raikwar, Nikita Polyanskii, Sebastian Müller
This paper is a Systematization of Knowledge (SoK) that focuses on Directed Acyclic Graph (DAG)-based consensus protocols in Distributed Ledger Technologies (DLTs). Our study evaluates their impact on performance and their tradeoffs concerning consistency, availability, and partition tolerance, as postulated by the CAP theorem. We delineate the key functionalities and tradeoffs of DAGbased consensus protocols, highlighting iterative improvements and deviations from foundational models. Additionally, we identify research gaps and suggest directions for future work to refine DAG-based consensus mechanisms.
Srisht Fateh Singh, Panagiotis Michalopoulos, Andreas Veneris
This paper introduces BAKUP, a smart contract insurance design for decentralized finance users to mitigate risks arising from platform vulnerabilities. While providing automated claim payout, BAKUP utilizes a modular structure to harmonize three key features: the platform's resilience against vulnerabilities, the flexibility of underwritten policies, and capital efficiency. An immutable core module performs capital accounting while ensuring robustness against external vulnerabilities, a customizable oracle module enables the underwriting of novel policies, and an optional and peripheral yield module allows users to independently manage additional yield. The implementation incorporates binary conditional tokens that are tradable on automated market maker (AMM)-based exchanges. Finally, the paper examines specific liquidity provision strategies for the conditional tokens, demonstrating that a conservative strategy and parameterization can effectively reduce the divergence loss of liquidity providers by more than 47 % compared to a naive strategy in the worst-case scenario.
Distributed ledger technology such as blockchain is considered essential for supporting large numbers of micro-transactions in the Machine Economy, which is envisioned to involve billions of connected heterogeneous and decentralized cyber-physical systems. This stresses the need for performance and scalability of distributed ledger technologies. Addressing this, sharding techniques that divide the blockchain network into multiple committees are a common approach to improve scalability. However, with current sharding approaches, costly cross-shard verification is needed to prevent double-spending. This article proposes a novel and more scalable distributed ledger method named ScaleGraph that implements dynamic sharding by using routing and logical proximity concepts from distributed hash tables. ScaleGraph addresses cybersecurity in terms of integrity and availability to support frequent micro-transactions between autonomous devices. Benefits of ScaleGraph include a total storage space complexity of \(O(t)\) , where \( t \) is the global number of transactions (assuming a constant replication degree). This space is sharded over \( N \) nodes so that each node needs \(O(t/N)\) storage in expectation, which provides a high level of concurrency and data localization as compared to other delegated consensus proposals. ScaleGraph allows for a dynamic grouping of validators that are selected based on a distance metric. We analyze the consensus requirements in such a dynamic setting and show that a synchronous consensus protocol allows shards to be smaller than an asynchronous one, and likely yields better performance. Moreover, we provide an experimental analysis of security aspects regarding the required size of the consensus groups with ScaleGraph. Our analysis shows that dynamic sharding based on proximity concepts brings attractive scalability properties in general, especially when the fraction of corrupt nodes is small.
Abstract. The purpose of a consensus protocol is to keep a distributed network of nodes “in sync,” even in the presence of an unpredictable communication network and adversarial behavior by some of the participating nodes. In the permissionless setting relevant to modern blockchain protocols, these nodes may be operated by a large number of unknown players, with each player free to use multiple identifiers and to start or stop running the protocol at any time. Establishing that a permissionless consensus protocol is “secure” thus requires both a distributed computing argument (that the protocol guarantees consistency and liveness unless the fraction of adversarial participation is sufficiently large) and an economic argument (that carrying out an attack would be prohibitively expensive for a potential attacker). There is a mature toolbox for assembling arguments of the former type; the goal of this paper is to lay the foundations for arguments of the latter type. For example, the Ethereum protocol is oft-claimed to be “more economically secure” after “the merge,” meaning in its current proof-of-stake incarnation relative to the (proof-of-work) original. What, formally, does this assertion mean? Is it true? Could there be alternative protocols that are “still more economically secure” than Ethereum? How do the answers depend on the assumptions imposed on, for example, the reliability of message delivery or the active participation of non-malicious players? An ideal permissionless consensus protocol would, in addition to satisfying standard consistency and liveness guarantees, render consistency violations prohibitively expensive for the attacker without collateral damage to honest participants—for example, by programatically confiscating an attacker’s resources without reducing the value of honest participants’ resources, as is the intention for slashing in a proof-of-stake protocol. We make this idea precise with our notion of the EAAC (expensive to attack in the absence of collapse) property and prove the following results: (1) In the synchronous and dynamically available setting (in which the communication network is reliable but nonmalicious players may be periodically inactive), with an adversary that controls at least one-half of the overall resources, no protocol can be EAAC. In particular, this result rules out EAAC for all typical longest-chain protocols (be they proof-of-work or proof-of-stake). (2) In the partially synchronous and quasi-permissionless setting (in which resource-controlling non-malicious players are always active but the communication network may suffer periods of unreliability), with an adversary that controls at least one-third of the overall resources, no protocol can be EAAC. In particular, slashing in a proof-of-stake protocol cannot achieve its intended purpose if message delays cannot be bounded a priori. (3) In the synchronous and quasi-permissionless setting, there is a proof-of-stake protocol with slashing that, provided the adversary controls less than two-thirds of the overall stake, satisfies the EAAC property. Thus, while only “classical security” is possible in the dynamically available or partially synchronous settings, proof-of-stake protocols with slashing can obtain additional “economic security” in the quasi-permissionless and synchronous settings. All three results are optimal with respect to the size of the adversary. With respect to Ethereum, our work formalizes the potential security benefits of proof-of-stake sybil-resistance coupled with slashing and the common belief that the merge has increased Ethereum’s economic security. Our work also provides mathematical justifications for several key design decisions behind the post-merge Ethereum protocol, ranging from long cooldown periods for unstaking to economic penalties for inactivity.
The dynamic and unpredictable nature of network environments poses a significant challenge for distributed systems, particularly those relying on consensus algorithms for state management and fault tolerance. To address this challenge, this article introduces a novel simulation model designed to study the impact of unstable network connections on clusters running consensus algorithms. The model is engineered to mimic varying degrees of network instability, including latency fluctuations and connection disruptions, which are characteristic of real-world distributed systems. Our proposed model represents a significant advancement in the simulation of distributed networks. It employs a sophisticated network emulation layer capable of generating a wide spectrum of unstable network conditions. The core of the model is a highly configurable consensus mechanism simulator that allows for the adjustment of key parameters such as heartbeat intervals, election timeouts, and message loss rates. This level of configurability enables a comprehensive analysis of consensus behaviors under different network scenarios. The article focuses on the methodology behind the development of the model, detailing the theoretical underpinnings and the implementation strategies used to ensure a realistic representation of network instability. We also discuss the potential applications of the model, which extend beyond academic research into practical domains where distributed ledger technologies and distributed databases are prevalent. Through the deployment of this model, researchers and system architects can gain deeper insights into the resilience and adaptability of consensus algorithms. The model serves as a tool for preemptively identifying and addressing potential issues in distributed systems, facilitating the development of more robust and reliable technologies. In summary, the article showcases the design and capabilities of a new model that enables an in-depth understanding of the delicate interplay between network instability and consensus efficiency. By focusing on the model itself, the article aims to lay a foundation for future studies and improvements in the field of distributed systems.
Lucian Trestioreanu, Flaviene Scheidt, Wazen M. Shbair, Jérôme François · 6 authors
With the large increase in the adoption of blockchain technologies, their underlying peer-to-peer networks must also scale with the demand. In this context, previous works highlighted the importance of ensuring efficient and resilient communication for the underlying consensus and replication mechanisms. However, they were mainly focused on mainstream, Proof-of-Work-based Distributed Ledger Technologies like Bitcoin or Ethereum. In this paper, the problem is investigated in the context of consensus-validation based blockchains, like the XRP Ledger. The latter relies on a Federated Byzantine Agreement (FBA) consensus mechanism which is proven to have a good scalability in regards to transaction throughput. However, it is known that significant increases in the size of the XRP Ledger network would be challenging to achieve. The main reason is the flooding mechanism used to disseminate the messages related to the consensus protocol, which creates many duplicates in the network. Squelching is a recent solution proposed for limiting this duplication, however, it was never evaluated quantitatively in real-life scenarios involving the XRPL production network. In this paper, our aim is to assess this mechanism using a real-life controllable testbed and the XRPL production network, to assess its benefit and compare it to alternative solutions relying on Named Data Networking and on a gossip-based approach.
This paper introduces the Proof of Sampling (PoSP) protocol, a Nash Equilibrium-based verification mechanism, and its application to decentralized machine learning inference through spML. Our protocol has a pure strategy Nash Equilibrium, compelling rational participants to act honestly. It economically disincentivizes dishonest behavior, making it costly for participants to compromise the network's integrity. In our spML protocol, we apply PoSP to decentralized inference for AI applications via a novel cryptographic protocol. The resulting protocol is much more efficient than zero knowledge proof based approaches. Moreover, we anticipate that the PoSP protocol could be effectively utilized for designing verification mechanisms within Actively Validated Services (AVS) in restaking solutions. We further expect that the PoSP protocol could be applied to a variety of other decentralized applications. Our approach enhances the reliability and efficiency of decentralized systems, paving the way for a new generation of decentralized applications.
Ulysse Pavloff, Yackolley Amoussou-Guenou, Sara Tucci-Piergiovanni
In May 2023, the Ethereum blockchain experienced its first inactivity leak, a mechanism designed to reinstate chain finalization amid persistent network disruptions. This mechanism aims to reduce the voting power of validators who are unreachable within the network, reallocating this power to active validators. This paper investigates the implications of the inactivity leak on safety within the Ethereum blockchain. Our theoretical analysis reveals scenarios where actions by Byzantine validators expedite the finalization of two conflicting branches, and instances where Byzantine validators reach a voting power exceeding the critical safety threshold of one-third. Additionally, we revisit the probabilistic bouncing attack, illustrating how the inactivity leak can result in a probabilistic breach of safety, potentially allowing Byzantine validators to exceed the one-third safety threshold. Our findings uncover how penalizing inactive nodes can compromise blockchain properties, particularly in the presence of Byzantine validators capable of coordinating actions.
In the realm of Distributed Ledgers (DLs), a solution to enhancing maximum peak throughput involves establishing multiple independent blockchains that evolve concurrently. However, an excess of parallel chains in comparison to the application's demands can result in increased latency in content delivery, squandered bandwidth, and heightened computational strain on network nodes.
This article examines the significant challenges encountered in implementing sharding within distributed replication systems. It identifies the impediments of achieving consensus among large participant sets, leading to scalability, throughput, and performance limitations. These issues primarily arise due to the message complexity inherent in consensus mechanisms. In response, we investigate the potential of sharding to mitigate these challenges, analyzing current implementations within distributed replication systems. Additionally, we offer a comprehensive review of replication systems, encompassing both classical distributed databases as well as Distributed Ledger Technologies (DLTs) employing sharding techniques. Through this analysis, the article aims to provide insights into addressing the scalability and performance concerns in distributed replication systems.
Smart contracts have played a pivotal role in the evolution of blockchains and Decentralized Applications (DApps). As DApps continue to gain widespread adoption, multiple smart contract languages have been and are being made available to developers, each with its distinctive features, strengths, and weaknesses. In this paper, we examine the smart contract languages used in major blockchain platforms, with the goal of providing a comprehensive assessment of their main properties. Our analysis targets the programming languages rather than the underlying architecture: as a result, while we do consider the interplay between language design and blockchain model, our main focus remains on language-specific features such as usability, programming style, safety and security. To conduct our assessment, we propose an original benchmark which encompasses a wide, yet manageable, spectrum of key use cases that cut across all the smart contract languages under examination. • We give an abstract overview of smart contract platforms, discussing the impact of different design choices. • We illustrate by examples how different design choices give rise to different programming styles for smart contracts. • We consider 6 leading smart contract languages: Solidity (Ethereum), Rust (Solana), Aiken (Cardano), PyTeal (Algorand), Move (Aptos), SmartPy (Tezos). • We develop an open-source benchmark of use cases of smart contracts, implemented in all the languages in our selection. • Based on our benchmark, we evaluate smart contract languages focussing on their security, code readability, usability, and functionalities.
Bank of Italy, Carlo Gola, Guido Befani, Patrizio Fiorenza · 7 authors
The work provides a method for classifying blockchains and crypto-assets, facilitating their comparison for business and regulatory purposes. Blockchains - and more generally systems based on Distributed Ledger Technology (DLT) - adopt different technologic configurations, each distinguished by the activities performed, technical characteristics, and governance structures. Particular noteworthy is the difference between some DLTs, which integrate automated organizational procedures with traditional decision-making processes, and others that adopt entirely algorithmic governance. Equally complex is the task of identifying types of crypto-assets, also known as digital tokens, generated and transferred through this technology. The work outlines the primary characteristics of DLTs and crypto-assets, utilizing ‘switching circuits’ to visually represent or express them in a simple formula. The proposed methodology, applicable both in the EU and in the US, untangles a given DLT/crypto ecosystem and reassembles it through logic maps, facilitating the identification of the technologic, economic, and legal features and overcoming the risk of a rigid and easily outdated taxonomy. The ultimate purpose of the paper is to propose a working method capable of accommodating every possible configuration of DLT and digital token and their potential evolutions. Practical examples of regulatory application and two case studies (Ethereum and Polkadot) are provided
Networked computing power is a critical utility in the era of artificial intelligence. This paper presents a novel Physical Infrastructure Finance (PinFi) protocol designed to facilitate the distribution of computing power within networks in a decentralized manner. Addressing the core challenges of coordination, pricing, and liquidity in decentralized physical infrastructure networks (DePIN), the PinFi protocol introduces a distinctive dynamic pricing mechanism. It enables providers to allocate excess computing resources to a "dissipative" PinFi liquidity pool, distinct from traditional DeFi liquidity pools, ensuring seamless access for clients at equitable, market-based prices. This approach significantly reduces the costs of accessing computing power, potentially to as low as 1% compared to existing services, while simultaneously enhancing security and dependability. The PinFi protocol is poised to transform the dynamics of supply and demand in computing power networks, setting a new standard for efficiency and accessibility.
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.