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プロトコルに成功裏に適用され、1万行を超えるCoqコードの機械的証明が完了しました。その中で、安全性と活性の検証のためのコード量はそれぞれ4000行と1700行に達しています。邵中教授は講演の中で次のように強調しました："現在、PoSコンセンサスプロトコルは一般的に、安全性、活性、分散化の三者を同時に満たすことが難しいというジレンマに直面しています。LiDOモデルは、このボトルネックを突破するために提案された体系的な解決策です。"

注目すべきは、邵中教授がチームを率いて世界初の形式的検証を通じて「バグのない」オペレーティングシステムCertiKOSを開発したことで、業界から「サイバー物理システムの安全性のマイルストーン」と称賛されていることです。この成果は、彼のチームがシステムセキュリティ分野での深い蓄積を示すものであり、今後の研究に堅固な基盤を提供しています。近年、邵中教授は研究の焦点をブロックチェーンセキュリティに移し、2017年にパートナーと共にブロックチェーンセキュリティ会社を設立し、形式的検証技術をスマートコントラクトとオンチェーンプロトコルの安全保障に応用することに取り組み、数千億ドル規模の暗号資産に安全保護を提供しています。

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

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