Web3 Scholars Summit: Yale Professor Debuts LiDO Model

At the 2025 Web3 Scholars Summit, Professor Zhao 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 mechanizable verifiable security and liveness proofs for complex Byzantine Fault Tolerance (BFT) consensus protocols, laying a technical foundation for the reliability and large-scale 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, their high implementation complexity often conceals potential vulnerabilities. To address this issue, the LiDO model innovatively proposes a three-layer refined verification framework:

1. Security abstraction layer: Maps protocols to a linearized state machine to ensure log consistency (security).
2. Active Assurance Layer: Introduces the "Pacemaker" mechanism to solve network latency issues through timeout broadcasting and round synchronization.
3. DAG Expansion Layer: Supports new DAG protocols such as Narwhal and Bullshark to achieve efficient validation 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 code, with the amount of code 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 achieving security, liveness, and decentralization simultaneously. The LiDO model is a systematic design solution proposed to break through this dilemma."

The team led by Professor Shao Zhong developed CertiKOS, the world's first "bug-free" operating system verified through formal verification, hailed as a "milestone in the security of cyber-physical systems." This achievement not only laid the foundation for related technologies but also showcased the team's profound accumulation in the field of system security. In recent years, Professor Shao Zhong has delved into blockchain security, and in 2017, he co-founded a security company with colleagues, introducing formal verification technology into the security assurance of smart contracts and on-chain protocols, providing security protection for cryptocurrency assets worth hundreds of billions of dollars.

LiDO has currently completed model 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 presentation, Professor Shao Zhong emphasized: "A trustworthy, secure, and verifiable network protocol stack will be the key path to a truly decentralized future."