Web3学者峰会上耶鲁教授发布革新的コンセンサスプロトコル検証モデル

2025年のWeb3学者サミットで、イェール大学コンピュータサイエンス学科の教授であるシャオ・ジョンは、「細分化されたコンセンサスプロトコルの安全性と活性証明：LiDOとその拡張」というタイトルの基調講演を行い、初めて彼のチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを公開しました。この画期的な成果は、複雑なビザンチン耐障害（BFT）コンセンサスプロトコルに対して機械的検証可能な安全性と活性証明を提供し、Web3エコシステムの信頼性とスケール化の発展のための技術的基盤を築くことを目指しています。

邵中教授は講演の中で、既存のコンセンサスプロトコル（例えばPBFT、Jolteon）が広く使われているにもかかわらず、実装の複雑さがしばしば潜在的な脆弱性を隠すことを指摘しました。この問題を解決するために、LiDOモデルは革新的に三層の細分化検証フレームワークを提案しました：

1. セキュリティ抽象層：プロトコルを線形化された状態機械にマッピングし、ログの整合性を確保する（安全性）；
2. 活性保障層："Pacemaker"メカニズムを導入し、タイムアウトブロードキャストとラウンド同期を通じてネットワーク遅延問題を解決する；
3. DAG拡張層：NarwhalやBullsharkなどの新興DAGプロトコルをサポートし、リーダーのないコンセンサスの効率的な検証を実現します。

現在、LiDOは産業用プロトコルJolteon（二段階BFT）および複数のDAGプロトコルに成功裏に適用され、1万行を超えるCoqコードの機械的証明が完了しました。その中で、安全性と活性の検証コードの量はそれぞれ4000行と1700行に達しています。邵中教授は講演で次のように強調しました："現在、PoSコンセンサスプロトコルは安全性、活性、分散化の3つを同時に実現することが難しいというジレンマに直面しています。LiDOモデルはこのジレンマを打破するために提案された体系的な設計方案です。"

グローバル初の形式的検証を通じて「無漏洞」オペレーティングシステムCertiKOSの開発者である邵中教授は、システムセキュリティ分野で深い蓄積を持っています。近年、彼は研究の焦点をブロックチェーンセキュリティに移し、2017年にパートナーと共にセキュリティ会社を設立し、形式的検証技術をスマートコントラクトとオンチェーンプロトコルのセキュリティ保障に導入し、大規模な暗号資産に安全を提供しています。

LiDOモデルは現在、設計と形式的検証を完了し、主流のパブリックチェーンおよび分散型プロトコルとの統合の可能性を探求し始めています。邵中教授は、彼らがWeb3.0における重要なメカニズムの検証に取り組んでおり、全周期の製品とサービスを提供し、Web3企業とエコシステムの長期的な発展戦略をより良く支援することを目指していると述べています。

講演の最後に、邵中教授は強調しました："信頼でき、安全で、検証可能なネットワークプロトコルスタックは、真の分散型未来への重要な道筋となるでしょう。"

! CertiKの共同創設者であるShao Zhong教授は、Web3 Scholars Summitに出席し、LiDOモデルを初めて公開しました