The Web3 Scholars Summit Reveals the Security Model of the Next Generation Consensus Protocol

At the recently held 2025 Web3 Scholars Summit, Professor Zhao Zhong from the Department of Computer Science at Yale University delivered a keynote speech titled "Refined Consensus Protocol Security and Liveness Proof: LiDO and Its Extensions," publicly unveiling the LiDO model and the LiDO-DAG extension framework developed by his team for the first time. This groundbreaking achievement aims to provide mechanizable verification of security and liveness proofs for complex Byzantine Fault Tolerance (BFT) consensus protocols, laying a technological foundation for the reliability and scalable development of the Web3 ecosystem.

Professor Shao Zhong pointed out in his speech that although existing consensus protocols such as PBFT and Jolteon are widely used, they often harbor potential vulnerabilities due to implementation complexity. To address this issue, the LiDO model innovatively proposed a three-layer refined verification framework:

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

Currently, LiDO has been successfully applied to the industrial-grade protocol Jolteon (two-phase BFT) and multiple DAG protocols, completing over ten thousand lines of mechanized proof in Coq code, with the code volume for security and liveness verification reaching 4000 lines and 1700 lines respectively. Professor Shao Zhong emphasized: "At present, PoS Consensus protocols generally face the dilemma of being unable to achieve security, liveness, and decentralization simultaneously. The LiDO model is a systematic design solution proposed to break this dilemma."

As the founder of CertiKOS, the world's first "bug-free" operating system verified through formal verification, Professor Zhong Shao has a deep accumulation of knowledge in the field of system security. This achievement not only laid the foundation for his work in security technology but also showcased his expertise in system security. In recent years, Professor Shao has shifted his research focus to blockchain security, dedicated to applying formal verification techniques to the security guarantees of smart contracts and on-chain protocols, providing security protection for hundreds of billions of dollars in crypto assets.

The LiDO model has currently completed its design and formal verification, and has begun exploring the integration possibilities with mainstream public chains and decentralized protocols. Professor Shao Zhong stated that they are committed to verifying key mechanisms in Web3.0 to provide full-cycle products and services, better supporting the long-term development strategy 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." This viewpoint highlights the importance of building a secure and reliable infrastructure for promoting the healthy development of the entire ecosystem in the Web3 era.