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年、邵中教授は弟子の顧荣辉教授と共に形式的検証技術をスマートコントラクトとオンチェーンプロトコルのセキュリティ保障分野に導入し、数千億ドル規模の暗号資産に安全を提供しました。

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

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