イェール大学の教授がWeb3学者サミットで初めてLiDOモデルを公開

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

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

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

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

邵中教授が率いるチームは以前にCertiKOSを開発しました。これは、形式的検証を通じて世界初の「脆弱性のない」オペレーティングシステムであり、「サイバーフィジカルシステムの安全性のマイルストーン」と見なされています。この成果は、システムセキュリティ分野での深い蓄積を示すだけでなく、その後のブロックチェーンセキュリティ分野での研究の基盤を築きました。2017年、邵中教授はブロックチェーンセキュリティの研究に深く取り組み、形式的検証技術をスマートコントラクトとオンチェーンプロトコルの安全保障に導入し、多くの暗号資産に安全保護を提供しました。

LiDOモデルは現在、設計と形式的検証を完了し、主流のパブリックチェーンおよび分散型プロトコルとの統合の可能性を探り始めています。邵中教授は、彼らがWeb3.0における重要なメカニズムの検証に取り組んでおり、全周期の製品とサービスを提供し、Web3企業とエコシステムの長期的な発展戦略をより良くサポートすることを目指していると述べています。講演の最後に、邵中教授は次のように強調しました："信頼できて、安全で、検証可能なネットワークプロトコルスタックは、真の分散型未来への重要な道筋となるでしょう。"

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