Last modified: Sat Oct 25 14:37:25 2025 GMT.
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 round-jumping 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.