CertiK联创邵中教授出席Web3学者峰会，首次公开LiDO模型

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企业和生态的长期发展战略。演讲最后，邵中教授强调：“可信、安全、可验证的网络协议栈，将是通向真正去中心化未来的关键路径。”