# Web3學者峯會上耶魯教授首次公開LiDO模型2025年Web3學者峯會近日召開，耶魯大學計算機科學系教授邵中發表了題爲《基於細化的共識協議安全性與活性證明：LiDO及其拓展》的主題演講，首次揭示了他的團隊開發的LiDO模型和LiDO-DAG擴展框架。這一創新成果旨在爲復雜的拜佔庭容錯（BFT）共識協議提供可機械化驗證的安全性和活性證明，爲Web3生態系統的可靠性和可擴展性發展奠定技術基礎。邵中教授在演講中指出，盡管現有的共識協議（如PBFT和Jolteon）被廣泛應用，但由於實現復雜性，它們常常隱藏着潛在的漏洞。爲解決這一問題，LiDO模型創新性地提出了三層細化驗證框架：1. 安全抽象層：將協議映射爲線性化狀態機，確保日志一致性（安全性）；2. 活性保障層：引入"Pacemaker"機制，通過超時廣播和輪次同步解決網路延遲問題；3. DAG擴展層：支持Narwhal、Bullshark等新興DAG協議，實現無領導者共識的高效驗證。目前，LiDO已成功應用於工業級協議Jolteon（兩階段BFT）和多個DAG協議，完成了超過10,000行Coq代碼的機械化證明，其中安全性和活性驗證的代碼量分別達到了4,000行和1,700行。邵中教授在演講中強調："當前，PoS共識協議普遍面臨安全性、活性與去中心化三者難以兼得的困境。LiDO模型正是爲打破這一困境而提出的系統性設計方案。"邵中教授及其團隊此前開發的CertiKOS是全球首個通過形式化驗證的"無漏洞"操作系統，被譽爲"網路物理系統安全的裏程碑"。這一成就不僅奠定了他們在系統安全領域的深厚積累，也展示了他們在這一領域的專業能力。近年來，邵中教授深入研究區塊鏈安全，於2017年與其學生顧榮輝教授共同將形式化驗證技術引入智能合約和鏈上協議的安全保障領域，爲數千億美元級的加密資產提供安全保護。LiDO目前已完成模型設計和形式化驗證，並開始探索與主流公鏈及去中心化協議的集成可能性。邵中教授表示，他們致力於驗證Web3.0中的關鍵機制，以提供全週期產品和服務，更好地支持Web3企業和生態的長期發展戰略。在演講結束時，邵中教授強調："可信、安全、可驗證的網路協議棧，將是通向真正去中心化未來的關鍵路徑。"
耶魯教授發布LiDO模型：Web3共識協議安全性驗證新框架
Web3學者峯會上耶魯教授首次公開LiDO模型
2025年Web3學者峯會近日召開，耶魯大學計算機科學系教授邵中發表了題爲《基於細化的共識協議安全性與活性證明：LiDO及其拓展》的主題演講，首次揭示了他的團隊開發的LiDO模型和LiDO-DAG擴展框架。這一創新成果旨在爲復雜的拜佔庭容錯（BFT）共識協議提供可機械化驗證的安全性和活性證明，爲Web3生態系統的可靠性和可擴展性發展奠定技術基礎。
邵中教授在演講中指出，盡管現有的共識協議（如PBFT和Jolteon）被廣泛應用，但由於實現復雜性，它們常常隱藏着潛在的漏洞。爲解決這一問題，LiDO模型創新性地提出了三層細化驗證框架：
目前，LiDO已成功應用於工業級協議Jolteon（兩階段BFT）和多個DAG協議，完成了超過10,000行Coq代碼的機械化證明，其中安全性和活性驗證的代碼量分別達到了4,000行和1,700行。邵中教授在演講中強調："當前，PoS共識協議普遍面臨安全性、活性與去中心化三者難以兼得的困境。LiDO模型正是爲打破這一困境而提出的系統性設計方案。"
邵中教授及其團隊此前開發的CertiKOS是全球首個通過形式化驗證的"無漏洞"操作系統，被譽爲"網路物理系統安全的裏程碑"。這一成就不僅奠定了他們在系統安全領域的深厚積累，也展示了他們在這一領域的專業能力。近年來，邵中教授深入研究區塊鏈安全，於2017年與其學生顧榮輝教授共同將形式化驗證技術引入智能合約和鏈上協議的安全保障領域，爲數千億美元級的加密資產提供安全保護。
LiDO目前已完成模型設計和形式化驗證，並開始探索與主流公鏈及去中心化協議的集成可能性。邵中教授表示，他們致力於驗證Web3.0中的關鍵機制，以提供全週期產品和服務，更好地支持Web3企業和生態的長期發展戰略。在演講結束時，邵中教授強調："可信、安全、可驗證的網路協議棧，將是通向真正去中心化未來的關鍵路徑。"