At the Web3 Scholars Summit, Yale Professor publicly presented the LiDO model for the first time.

The Web3 Scholars Summit of 2025 is being held today, and Professor Zhao Zhong from Yale University's Department of Computer Science delivered a keynote speech titled "A Refined Consensus Protocol's Security and Liveness Proof: LiDO and its Extensions." He publicly unveiled the LiDO model developed by his team and the LiDO-DAG extension framework 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 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 and 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 refined verification framework:

1. Security abstraction layer: Maps protocols to a linearized state machine, ensuring log consistency (security);
2. Active Assurance Layer: Introduces 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 validation without a leader consensus.

Currently, LiDO has been successfully applied to the industrial-grade protocol Jolteon (two-phase BFT) and several DAG protocols, completing mechanical proofs of over ten thousand lines of Coq code, with safety and liveness verification code amounts reaching 4000 lines and 1700 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."

As the developer of CertiKOS, the world's first "bug-free" operating system verified by formal methods, Professor Zhao Zhong has accumulated profound expertise in system security. This achievement is hailed as a "milestone in cyber-physical system security." In recent years, Professor Zhao Zhong has shifted his research focus to blockchain security, co-founding a security company in 2017 with his disciple Professor Gu Ronghui, bringing formal verification technology into the security assurance 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 the 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."