Web3学者峰会でイェール大学の教授が初めてLiDOモデルを公開

最近開催された2025年Web3学者サミットで、イェール大学コンピュータサイエンス学科の教授である邵中が「細化に基づくコンセンサスプロトコルのセキュリティと活性の証明：LiDOおよびその拡張」のテーマで基調講演を行い、初めて公に彼のチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを紹介しました。この革新的な成果は、複雑なビザンチン耐障害（BFT）コンセンサスプロトコルに対して機械的に検証可能なセキュリティと活性の証明を提供することを目指し、Web3エコシステムの信頼性と大規模な発展への道を切り開くものです。

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

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

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

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

邵中教授が率いるチームは、以前にCertiKOSを開発しました。これは、形式的検証を通じて初めての「脆弱性のない」オペレーティングシステムであり、業界からは「サイバーフィジカルシステムの安全のマイルストーン」と称されています。この成果は、関連技術の基盤を確立するだけでなく、システムセキュリティ分野におけるチームの深い蓄積を示しています。近年、邵中教授はブロックチェーンセキュリティの研究を深め、2017年に同僚と共にセキュリティ会社を設立し、形式的検証技術をスマートコントラクトとオンチェーンプロトコルの安全保障に導入し、数千億ドル規模の暗号資産に安全保護を提供しています。

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