2025香港Web3嘉年华不仅是技术交流的盛会，也是学术研究与行业实践交汇的重要舞台。在4月8日举行的Web3学者峰会上，以太坊联合创始人Vitalik Buterin、CertiK联合创始人兼耶鲁大学计算机科学系教授邵中，以及多位行业领袖与顶尖学者悉数出席，共同探讨Web3的前沿发展。
CertiK联合创始人邵中教授发表了备受期待的主题演讲，向全球Web3社区首次公开了CertiK团队的最新学术成果——LiDO模型及LiDO-DAG扩展框架。这一创新性框架为复杂的拜占庭容错(BFT)共识协议提供了可机械化验证的安全性与活性证明，成为本届嘉年华的学术亮点，也标志着CertiK在区块链安全领域的又一重大突破。
邵中教授在演讲中指出，当前广泛应用的共识协议(如PBFT、Jolteon)因实现复杂度高，往往隐藏潜在漏洞，难以在安全性、活性与去中心化之间取得平衡。为解决这一难题，LiDO模型创新性地提出了三层细化验证框架：安全抽象层将协议映射为线性化状态机，确保日志一致性；活性保障层引入“Pacemaker”机制，通过超时广播和轮次同步破解网络延迟难题；DAG扩展层则支持Narwhal、Bullshark等新兴DAG协议，实现无领导者共识的高效验证。邵教授详细讲解了LiDO如何应用于工业级协议Jolteon(两阶段BFT)及多个DAG协议，已完成超万行Coq代码的机械化证明，其中安全性验证代码达4000行，活性验证代码达1700行。他表示：“PoS共识协议普遍面临三难困境，而LiDO正是为打破这一困境设计的系统性方案。”
LiDO的研发背景源于邵中教授在系统安全领域的深厚积累。他带领团队开发的CertiKOS，是全球首个通过形式化验证的“无漏洞”操作系统，被誉为网络物理系统安全的里程碑。这一技术根基也为CertiK的创立奠定了基础。2017年，邵中教授与弟子顾荣辉教授共同创立CertiK，将形式化验证技术引入智能合约和链上协议的安全保障，至今已为千亿美元级的加密资产提供了保护。LiDO模型的亮相，不仅是CertiK学术研究的最新成果，也预示着其在Web3协议安全验证上的更大潜力。邵教授透露，LiDO已完成模型设计与形式化验证，并开始探索与主流公链及去中心化协议的集成可能性。他强调：“可信、安全、可验证的网络协议栈，是通向真正去中心化未来的关键路径。”
在嘉年华期间，CertiK的展位也成为技术交流的热门场所，吸引了众多开发者、企业代表和投资者的关注。CertiK以LiDO为代表的学术突破，不仅提升了Web3协议的可靠性，也为生态的长期发展注入了信心，展现了其作为行业领导者的责任与远见。
