On April 8, at the Web3 Scholars Conference 2025 held in Hong Kong, Zhong Shao, professor of computer science at Yale University and co-founder of CertiK, delivered a keynote speech titled Security and Liveness Proofs of Consensus Protocols Based on Refinement: LiDO and Its Extensions, and for the first time, he unveiled the LiDO model and LiDO-DAG extension framework developed by his team. This breakthrough is designed to provide mechanized verifiable security and liveness proofs for complex Byzantine Fault Tolerant (BFT) consensus protocols, laying a 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, they often hide potential vulnerabilities due to their complex implementation. To solve this problem, the LiDO model innovatively proposes a three-layer detailed verification framework:
Security abstraction layer: maps the protocol into a linearized state machine to ensure log consistency (security);
Activeness guarantee layer: Introducing the Pacemaker mechanism to solve the problem of network delay through timeout broadcast 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-phase BFT) and multiple DAG protocols, completing the mechanized proof of more than 10,000 lines of Coq code, with 4,000 lines of security and 1,700 lines of activity verification code respectively. Currently, PoS consensus protocols generally face the dilemma of having difficulty in achieving security, activity and decentralization at the same time, Professor Shao Zhong pointed out in his speech. The LiDO model is a systematic design solution proposed to break this dilemma.
CertiKOS, developed by Professor Shao Zhong and his team, is the worlds first vulnerable operating system that has passed formal verification and is hailed as a milestone in cyber-physical system security. This achievement not only laid the technical foundation for the 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, safeguarding the security of $100 billion worth of encrypted assets.
LiDO has 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 to better support the long-term development strategy of Web3 enterprises and ecosystems. At the end of his speech, Professor Shao Zhong emphasized: A trusted, secure, and verifiable network protocol stack will be the key path to a truly decentralized future.
