【2025 年 4 月 8 日，香港】在今日举行的 2025 年 Web3 学者峰会（Web3 Scholars Conference 2025）上，耶鲁大学计算机科学系教授、CertiK 联合创始人邵中发表了题为《基于细化的共识协议安全性与活性证明：LiDO 及其拓展》的主题演讲，首次公开了其团队研发的 LiDO 模型及 LiDO-DAG 扩展框架。这一突破性成果旨在为复杂拜占庭容错（BFT）共识协议提供可机械化验证的安全性与活性证明，为 Web3 生态的可靠性与规模化发展奠定技术基石。

在本次演讲中，邵中教授指出，现有共识协议（如 PBFT、Jolteon）虽广泛应用，但因实现复杂常隐藏潜在漏洞。为解决这一问题，LiDO 模型创新性地提出三层细化验证框架：

安全抽象层：将协议映射为线性化状态机，确保日志一致性（安全性）；

活性保障层：引入“Pacemaker”机制，通过超时广播和轮次同步破解网络延迟难题；

DAG 扩展层：支持 Narwhal、Bullshark 等新兴 DAG 协议，实现无领导者共识的高效验证。

目前，LiDO 已成功应用于工业级协议 Jolteon（两阶段 BFT）及多个 DAG 协议，完成超万行 Coq 代码的机械化证明，安全性与活性验证代码量分别达 4000 行和 1700 行。“当前，PoS 共识协议普遍面临安全性、活性与去中心化三者难以兼得的困境，”邵中教授在演讲中指出。“LiDO 模型正是为打破这一困境而提出的系统性设计方案。”

邵中教授带领团队研发的 CertiKOS，是全球首个通过形式化验证的“无漏洞”操作系统，被誉为“网络物理系统安全的里程碑”。这一成就不仅奠定了安全公司 CertiK 的技术根基，也彰显了其在系统安全领域的深厚积累。近年来，邵中教授深耕区块链安全，于 2017 年与弟子顾荣辉教授共同创立 CertiK，将形式化验证技术引入智能合约与链上协议的安全保障，护航千亿美元级加密资产安全。

LiDO 当前已完成模型设计与形式化验证，并开始探索与主流公链及去中心化协议的集成可能性。邵中教授表示，CertiK 致力于验证 Web3.0 中的关键机制，以提供全周期产品和服务，更好地支持 Web3 企业和生态的长期发展战略。演讲最后，邵中教授强调：“可信、安全、可验证的网络协议栈，将是通向真正去中心化未来的关键路径。”