Mechanized Safety and Liveness Proofs for the Mysticeti Consensus Protocol Under the LiDO-DAG Framework

Directed acyclic graphs (DAG) have recently become a popular building block for high-throughput consensus protocols used in blockchains. Mysticeti is a state-of-the-art DAG-based consensus protocol that is currently deployed in the Sui blockchain and the IOTA blockchain. Compared to previous protocols, Mysticeti achieves lower commit latency by eliminating reliable broadcast and increasing leader vertex frequency. However, this comes at the cost of significantly more complex security proofs than previous protocols. In fact, shortly after Mysticeti was published, flaws were found in its liveness proof, leaving the correctness of the protocol uncertain. In this work, we resolve the controversy around correctness of Mysticeti by presenting the first complete analysis of the safety and liveness properties of Mysticeti. Our key finding is that, unlike previous DAG-based protocols like Narwhal and Bullshark, liveness of Mysticeti is highly sensitive to the roundjumping behavior of honest participants. If honest processes are allowed to jump over rounds arbitrarily, then we present an explicit counterexample to the liveness of Mysticeti: an infinite trace where no data blocks are ever committed. We then introduce a simple restriction on the round-jumping behavior, and show that our modification is sufficient to restore liveness of Mysticeti. We mechanized proofs of safety and liveness of Mysticeti under the LiDO-DAG framework, an abstract model of DAG-based consensus protocols proposed by Qiu et al., confirming that our modified protocol is fully correct. We also audited the current implementation of Mysticeti in the Sui blockchain and found it is susceptible to the described liveness bug. We have contacted Mysten Labs and are working with them to fix the liveness issues.