4 月 8 日，在香港舉行的 2025 年Web3學者高峰會（Web3 Scholars Conference 2025）上，耶魯大學電腦科學系教授、CertiK 聯合創始人邵中發表了題為《基於細化的共識協議安全性與活性證明：LiDO 及其拓展框架》的主題演講，首次公開了其團隊開發的 LiDO-D 模型。這項突破性成果旨在為複雜拜占庭容錯（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企業和生態的長期發展策略。演講最後，邵中教授強調：“可信、安全、可驗證的網路協議棧，將是通往真正去中心化未來的關鍵路徑。”
