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

At the Web3 Scholars Conference 2025 held today, Shao Zhong, a professor in the Department of Computer Science at Yale University and co-founder of CertiK, delivered a keynote speech entitled "Proof of Security and Activity of Consensus Protocols Based on Refinement: LiDO and Its Extensions", revealing the LiDO model and LiDO-DAG extension framework developed by his team for the first time. This breakthrough achievement aims to provide mechanically verifiable proof of security and liveness for the complex Byzantine Fault Tolerance (BFT) consensus protocol, laying a technical foundation for the reliability and large-scale development of the Web3 ecosystem.

In this speech, Professor Shao Zhong pointed out that existing consensus protocols (such as PBFT, Jolteon) are widely used but often hide potential vulnerabilities due to their complex implementation. 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, ensuring log consistency (security);
• Active Security 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, achieving efficient verification of leaderless consensus.

Currently, LiDO has been successfully applied to the industrial-grade protocol Jolteon (two-stage BFT) and several DAG protocols, completing the mechanized proof of over ten thousand lines of Coq code, with safety and liveness verification code totals reaching 4000 lines and 1700 lines respectively. "At present, PoS consensus protocols generally face the dilemma of achieving security, 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 Zhong Shao and his team developed CertiKOS, the world's first "bug-free" operating system verified through formal methods, hailed as a "milestone in cyber-physical system security". This achievement not only lays the technical foundation for the security company CertiK but also showcases its profound accumulation in the field of system security. In recent years, Professor Zhong Shao has focused on blockchain security, and in 2017, he co-founded CertiK with his disciple Professor Gu Ronghui, introducing formal verification technology to ensure the security of smart contracts and on-chain protocols, safeguarding the security of hundreds of billions of dollars in crypto assets.

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 CertiK is 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 trusted, secure, and verifiable network protocol stack will be the key path to a truly decentralized future."