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(2段階BFT)と複数のDAGプロトコルへの適用に成功しており、10,000行以上のCoqコード、4,000行のセキュリティ、1,700行のアクティビティ検証コードの機械化された証明を完了しています。 「現在、PoSコンセンサスプロトコルは一般的に、セキュリティ、実行可能性、分散化のジレンマに直面しています」とShao Zhong教授はスピーチで指摘しました。 「LiDOモデルは、このジレンマを打破するための体系的な設計ソリューションです。」邵中教授が率いるチームが開発したCertiKOSは、世界初の形式的検証を通じて「バグのない」オペレーティングシステムであり、「サイバー物理システムセキュリティのマイルストーン」と称されています。この成果は、セキュリティ会社CertiKの技術的基盤を確立しただけでなく、システムセキュリティ分野での彼らの深い蓄積をも示しています。近年、邵中教授はブロックチェーンセキュリティに専念し、2017年に弟子の顧荣辉教授と共にCertiKを設立し、形式的検証技術をスマートコントラクトとオンチェーンプロトコルのセキュリティ保障に導入し、数十億ドル規模の暗号資産の安全を守っています。LiDOは現在、モデル設計と形式化検証を完了し、主流のパブリックチェーンおよび分散型プロトコルとの統合の可能性を探り始めています。邵中教授は、CertiKがWeb3.0における重要なメカニズムの検証に取り組んでおり、全周期の製品とサービスを提供し、Web3企業とエコシステムの長期的な発展戦略をより良くサポートすることを目指していると述べました。講演の最後に、邵中教授は「信頼できる、安全で、検証可能なネットワークプロトコルスタックは、真の分散型未来への重要な道筋となるでしょう。」と強調しました。
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(2段階BFT)と複数のDAGプロトコルへの適用に成功しており、10,000行以上のCoqコード、4,000行のセキュリティ、1,700行のアクティビティ検証コードの機械化された証明を完了しています。 「現在、PoSコンセンサスプロトコルは一般的に、セキュリティ、実行可能性、分散化のジレンマに直面しています」とShao Zhong教授はスピーチで指摘しました。 「LiDOモデルは、このジレンマを打破するための体系的な設計ソリューションです。」
邵中教授が率いるチームが開発したCertiKOSは、世界初の形式的検証を通じて「バグのない」オペレーティングシステムであり、「サイバー物理システムセキュリティのマイルストーン」と称されています。この成果は、セキュリティ会社CertiKの技術的基盤を確立しただけでなく、システムセキュリティ分野での彼らの深い蓄積をも示しています。近年、邵中教授はブロックチェーンセキュリティに専念し、2017年に弟子の顧荣辉教授と共にCertiKを設立し、形式的検証技術をスマートコントラクトとオンチェーンプロトコルのセキュリティ保障に導入し、数十億ドル規模の暗号資産の安全を守っています。
LiDOは現在、モデル設計と形式化検証を完了し、主流のパブリックチェーンおよび分散型プロトコルとの統合の可能性を探り始めています。邵中教授は、CertiKがWeb3.0における重要なメカニズムの検証に取り組んでおり、全周期の製品とサービスを提供し、Web3企業とエコシステムの長期的な発展戦略をより良くサポートすることを目指していると述べました。講演の最後に、邵中教授は「信頼できる、安全で、検証可能なネットワークプロトコルスタックは、真の分散型未来への重要な道筋となるでしょう。」と強調しました。