Web3 Scholars Summit: Yale Professor Unveils LiDO Model to Enhance Consensus Protocol Security

At the 2025 Web3 Scholars Summit, Professor Zhao Zhong from the Department of Computer Science at Yale University delivered a keynote speech titled "Security and Liveness Proofs of Refined Consensus Protocols: LiDO and its Extensions," introducing for the first time the LiDO model and LiDO-DAG extension framework developed by his team. This innovative achievement aims to provide mechanizable verification of security and liveness proofs for complex Byzantine Fault Tolerance (BFT) consensus protocols, laying a technical foundation for the reliability and scalability of the Web3 ecosystem.

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

1. Security Abstraction Layer: Maps the protocol to a linearized state machine to ensure log consistency (security).
2. Active Guarantee Layer: Introduce the "Pacemaker" mechanism to address network latency 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) and several DAG protocols, completing more than 10,000 lines of mechanized proof in Coq code, with the code for safety and liveness verification reaching 4,000 lines and 1,700 lines respectively. Professor Shao Zhong emphasized in his speech: "At present, PoS Consensus protocols generally face the dilemma of being unable to achieve safety, liveness, and decentralization simultaneously. The LiDO model is a systematic design solution proposed to break this dilemma."

It is worth mentioning that Professor Shao Zhong led a team to develop CertiKOS, the world's first "bug-free" operating system verified through formal methods, which has been hailed as a "milestone in the security of cyber-physical systems." This achievement not only solidifies its profound foundation in the field of system security but also provides a solid basis for subsequent research in blockchain security. In 2017, Professor Shao Zhong and his student Professor Gu Ronghui jointly introduced formal verification technology into the field of security assurance for smart contracts and on-chain protocols, providing security protection for cryptocurrency assets worth billions of dollars.

The LiDO model has currently completed its design and formal verification, and is 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 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 pathway to a truly decentralized future." This viewpoint highlights the significant importance of the LiDO model in promoting the development of Web3 technology and security assurance.