Professor Shao Zhong, co-founder of CertiK, attended the Web3 Scholars Summit and publicly introduced the LiDO model for the first time.

On April 8, at the Web3 Scholars Conference 2025 held in Hong Kong, Professor Shao Zhong from Yale University's Department of Computer Science and co-founder of CertiK delivered a keynote speech titled "Security and Liveness Proof of Refined Consensus Protocol: LiDO and Its Extensions", unveiling for the first time the LiDO model and its LiDO-DAG extension framework developed by his team. This groundbreaking achievement aims to provide mechanizable verification of security and liveness proofs for complex Byzantine fault tolerance (BFT) consensus protocols, laying a technological foundation for the reliability and scalable development of the Web3 ecosystem.

In this presentation, Professor Shao Zhong pointed out that existing consensus protocols (such as PBFT and Jolteon) are widely used, but their complex implementations often hide potential vulnerabilities. To address this issue, the LiDO model innovatively proposes a three-layer refined verification framework:

Security Abstraction Layer: Maps the protocol to a linearized state machine to ensure log consistency (security);

Active Assurance Layer: Introduces the "Pacemaker" mechanism to solve the network delay problem through timeout broadcasting and round synchronization;

DAG Extension Layer: Supports emerging DAG protocols such as Narwhal and Bullshark, enabling efficient validation of leaderless Consensus.

Currently, LiDO has been successfully applied to the industrial-grade protocol Jolteon (two-stage BFT) and multiple DAG protocols, completing mechanical proof of over ten thousand lines of Coq code, with safety and liveness verification code reaching 4000 lines and 1700 lines respectively. "Currently, PoS consensus protocols generally face the dilemma of being unable to achieve safety, liveness, and decentralization simultaneously," Professor Shao Zhong pointed out in his speech. "The LiDO model is a systematic design solution proposed to break this dilemma."

Professor Shao Zhong and his team 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 technical foundation for the security company CertiK but also highlighted its profound accumulation in the field of system security. In recent years, Professor Shao Zhong has focused on blockchain security, co-founding CertiK with his disciple Professor Gu Ronghui in 2017, introducing formal verification technology to ensure the security of smart contracts and on-chain protocols, safeguarding the security of cryptocurrency assets worth tens of billions.

LiDO has currently completed model design and formal verification, and is beginning to explore integration possibilities with mainstream public chains and decentralized protocols. Professor Shao Zhong stated that CertiK is committed to verifying the 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."