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

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

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

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

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

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

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

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