At the Web3 Scholars Conference 2025 held today, Professor Shao Zhong from Yale University's Department of Computer Science and co-founder of CertiK delivered a keynote speech titled "Refined Consensus Protocol Security and Liveness Proof: LiDO and Its Extensions," where he publicly introduced the LiDO model and the LiDO-DAG extension framework developed by his team for the first time. This groundbreaking achievement aims to provide mechanizable verification of security and liveness for complex Byzantine Fault Tolerance (BFT) consensus protocols, laying a technical foundation for the reliability and scalable development of the Web3 ecosystem.

In his speech, Professor Shao pointed out that existing consensus protocols (such as PBFT and Jolteon) are widely used but often hide potential vulnerabilities due to their complex implementations. 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);
• Liveness Assurance Layer: Introduces a "Pacemaker" mechanism to tackle network latency issues through timeout broadcasting and round synchronization;
• DAG Extension Layer: Supports emerging DAG protocols like Narwhal and Bullshark, enabling efficient verification of leaderless consensus.

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

The CertiKOS developed by Professor Shao and his team is the world's first "bug-free" operating system verified through formal verification, hailed as a "milestone in cyber-physical system security." This achievement not only establishes the technical foundation for the security company CertiK but also highlights its deep accumulation in the field of system security. In recent years, Professor Shao has focused on blockchain security, co-founding CertiK with his student Professor Gu Ronghui in 2017, introducing formal verification technology into the security assurance 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 integration possibilities with mainstream public chains and decentralized protocols. Professor Shao 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 strategy of Web3 enterprises and ecosystems. At the end of his speech, Professor Shao emphasized, "A trustworthy, secure, and verifiable network protocol stack will be the key path to a truly decentralized future."

免责声明：本文章仅代表作者个人观点，不代表本平台的立场和观点。本文章仅供信息分享，不构成对任何人的任何投资建议。用户与作者之间的任何争议，与本平台无关。如网页中刊载的文章或图片涉及侵权，请提供相关的权利证明和身份证明发送邮件到support@aicoin.com，本平台相关工作人员将会进行核查。