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システムが、形式的検証を通じて世界初の"バグのない"オペレーティングシステムであり、"サイバーフィジカルシステムの安全性のマイルストーン"と称賛されていることです。この成果は、彼のチームがシステムセキュリティ分野での深い蓄積を示すだけでなく、今後のブロックチェーンセキュリティ研究のための強固な基盤を築いています。

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

講演の終わりに、邵中教授は次のように強調しました："信頼でき、安全で、検証可能なネットワークプロトコルスタックが、真の分散型未来への重要な道筋となるでしょう。"この見解は、Web3技術の発展を推進する上でのLiDOモデルの重要な役割を浮き彫りにし、未来の分散型システムの安全性と信頼性に新しい視点と方法を提供しています。

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