The LiDO model unveiled for the first time at the Web3 Scholars Summit: providing mechanized verification for complex Consensus protocols.

At the 2025 Web3 Scholars Summit, Professor Zhao Zhong from Yale University's Department of Computer Science delivered a keynote speech titled "Safety and Liveness Proofs of Refined Consensus Protocols: 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 mechanically verifiable safety and liveness proofs for complex Byzantine Fault Tolerant (BFT) consensus protocols, laying the 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) have been 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 the protocol to a linearized state machine, ensuring 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 multiple DAG protocols, completing the mechanized proof of over 10,000 lines of Coq code, with the security and liveness verification code amounting to 4,000 lines and 1,700 lines respectively. Professor Shao Zhong emphasized: "Currently, 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 main developer of CertiKOS, the world's first "bug-free" operating system verified by formal methods, Professor Zhong Shao has accumulated extensive experience in the field of system security. This achievement not only establishes his position in the field of security technology but also highlights his team's expertise in system security. In recent years, Professor Zhong Shao has shifted his research focus to blockchain security and co-founded a company in 2017 with partners that specializes in blockchain security, introducing formal verification technology to ensure the security of smart contracts and on-chain protocols, providing security protection for cryptocurrency assets worth hundreds of billions.

The LiDO model has now 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 validating 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 pathway to a truly decentralized future."