The Web3 Scholars Summit Focuses on New Consensus Protocol Security Verification Framework

At the recently held 2025 Web3 Scholars Summit, Professor Shao Zhong from Yale University's Department of Computer Science delivered a keynote speech titled "Security and Liveness Proofs of Refined Consensus Protocols: LiDO and Its Extensions," where he publicly introduced the LiDO model and the LiDO-DAG extension framework developed by his team for the first time. This innovative achievement aims to provide mechanizable verification of the security and liveness of complex Byzantine Fault Tolerance (BFT) consensus protocols, laying a solid technical 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, Jolteon) are widely used, they often hide potential vulnerabilities due to implementation complexity. To address this issue, the LiDO model innovatively proposed a three-layer refinement verification framework:

1. Security Abstraction Layer: Maps the protocol to a linearized state machine to ensure log consistency (security);
2. Active Assurance Layer: Introduce the "Pacemaker" mechanism to solve the network latency problem 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 over ten thousand lines of mechanized proof in Coq, with the code for safety and liveness verification amounting to 4000 lines and 1700 lines respectively. Professor Shao Zhong emphasized: "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 through this bottleneck."

As the global leader in the development of the "bug-free" operating system CertiKOS through formal verification, Professor Zhao Zhong and his team have accumulated profound technical strength in the field of system security. This achievement not only lays a solid foundation for their subsequent research but also demonstrates their outstanding contributions in the field of system security. In recent years, Professor Zhao Zhong has shifted his research focus to blockchain security, committed to applying formal verification technology to ensure the security of smart contracts and on-chain protocols, providing security protection for billions of dollars in crypto assets.

The LiDO model has now completed 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 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."