Professor Shao Zhong, CertiK, attended the Web3 Scholars Summit and released the LiDO model for the first time

At the 2025 Web3 Scholars Conference (Web3 Scholars Conference 2025) held today, Shao Zhong, professor of 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 Expansion", and for the first time disclosed the LiDO model and LiDO-DAG expansion framework developed by his team. This breakthrough achievement aims to provide mechanized verified security and activity proof for the complex Byzantine fault tolerance (BFT) consensus protocol, laying the technical foundation for the reliability and scale development of the Web3 ecosystem.

In this speech, Professor Shao Zhong pointed out that although existing consensus protocols (such as PBFT and Jolteon) are widely used, potential vulnerabilities often hide due to complex implementation. To solve this problem, LiDO model innovatively proposes a three-layer detailed verification framework:

• Security abstraction layer: maps protocols to linearized state machines to ensure log consistency (security);
• Active guarantee 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 to achieve efficient verification of leaderless consensus.

At present, LiDO has been successfully applied to the industrial-grade protocol Jolteon (two-stage BFT) and multiple DAG protocols, completing the mechanized proof of more than 10,000 lines of Coq code, with the security and activity verification code volumes reaching 4,000 lines and 1,700 lines respectively. "At present, PoS consensus protocols generally face the dilemma of being difficult to have both security, activity and decentralization," Professor Shao Zhong pointed out in his speech. "The LiDO model is a systematic design proposal to break this dilemma."

CertiKOS, developed by Professor Shao Zhong, led the team, is the world's first "vulnerable" operating system that has passed formal verification and is known as a "mile mark in the security of network physical system." This achievement not only laid the technical foundation of security company CertiK, but also demonstrated its deep accumulation in the field of system security. In recent years, Professor Shao Zhong has been deeply involved in blockchain security. In 2017, he co-founded CertiK with his disciple Professor Gu Ronghui, introducing formal verification technology into the security of smart contracts and on-chain protocols to escort the security of crypto assets of hundreds of billions of dollars.

LiDO has currently completed model design and formal verification, and has begun to explore the possibility of integration with mainstream public chains and decentralized protocols. Professor Shao Zhong said that CertiK is committed to verifying the key mechanisms in Web3.0 to provide full-cycle products and services and better support the long-term development strategy of Web3 enterprises and ecosystems. At the end of the speech, Professor Shao Zhong emphasized: "A credible, secure and verifiable network protocol stack will be the key path to a truly decentralized future."