Yale Professor Shares New Model for Consensus Protocol Security at the Web3 Scholars Summit

Recently, the 2025 Web3 Scholars Summit was held as scheduled. At the conference, Professor Shao Zhong from Yale University's Department of Computer Science delivered a keynote speech titled "Refined Consensus Protocol Security and Liveness Proof: LiDO and its Extensions," introducing to the public for the first time the LiDO model and the LiDO-DAG extension framework developed by his team. This innovative achievement aims to provide mechanically verifiable security and liveness proofs for complex Byzantine Fault Tolerant (BFT) consensus protocols, laying the technical foundation for the reliability and scalability development of the Web3 ecosystem.

Professor Shao Zhong pointed out in his speech that despite the widespread application of existing consensus protocols (such as PBFT and Jolteon), they often conceal potential vulnerabilities due to implementation complexity. To address this issue, the LiDO model proposes an innovative three-layer refined verification framework:

1. Security abstraction layer: Mapping the protocol to a linearized state machine to ensure log consistency (security);
2. Active Assurance Layer: Introduce the "Pacemaker" mechanism to solve network delay issues through timeout broadcasting and round synchronization;
3. DAG Extension Layer: Supports emerging DAG protocols such as Narwhal and Bullshark, achieving efficient verification of leaderless Consensus.

Currently, LiDO has been successfully applied to the industrial-grade protocol Jolteon (two-phase BFT) as well as several DAG protocols, completing over 10,000 lines of Coq code mechanized proofs, with the code volume for safety and liveness verification reaching 4,000 lines and 1,700 lines respectively. Professor Shao Zhong emphasized in his speech: "Currently, PoS Consensus protocols generally face the dilemma of being unable to achieve safety, liveness, and decentralization simultaneously. The LiDO model is precisely a systematic design solution proposed to break this dilemma."

It is worth mentioning that the team led by Professor Shao Zhong previously developed CertiKOS, which is the world's first "bug-free" operating system verified through formal verification, hailed as a "milestone in cyber-physical system security." This achievement not only demonstrates its profound accumulation in the field of system security but also lays the foundation for subsequent research in blockchain security. In 2017, Professor Shao Zhong and his disciple Professor Gu Ronghui jointly introduced formal verification technology into the security assurance field of smart contracts and on-chain protocols, providing security protection for hundreds of billions of dollars worth of crypto assets.

The LiDO model has now completed its design and formal verification, and has begun to explore the integration possibilities with mainstream public chains and decentralized protocols. Professor Shao Zhong stated that they are committed to validating the key mechanisms in Web3.0 to provide full-cycle products and services, better supporting the long-term development strategies of Web3 enterprises and ecosystems. At the end of the speech, Professor Shao Zhong emphasized: "A trustworthy, secure, and verifiable network protocol stack will be the key path to a truly decentralized future."