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

2025年のWeb3学者サミットで、イェール大学コンピュータサイエンス学科の教授であるシャオ・ジョンが「洗練されたコンセンサスプロトコルの安全性と活性証明：LiDOとその拡張」というタイトルの基調講演を行い、彼のチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを初めて公開しました。この画期的な成果は、複雑なビザンチン耐障害（BFT）コンセンサスプロトコルに対して機械的に検証可能な安全性と活性証明を提供することを目的としており、Web3エコシステムの信頼性とスケールの発展のための技術的基盤を築くことを目指しています。

邵中教授は、現行の合意プロトコルであるPBFTなどが広く使用されているが、実装が複雑なために潜在的な脆弱性が隠れていることを指摘しました。この問題を解決するために、LiDOモデルは革新的に三層の詳細な検証フレームワークを提案しました。

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

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

邵中教授が率いるチームが開発したCertiKOSは、世界初の形式的検証を受けた「バグのない」オペレーティングシステムであり、「サイバー物理システムの安全性のマイルストーン」と称されています。この成果は、システムセキュリティの分野における深い蓄積を確立するだけでなく、今後の研究に強固な基盤を提供しました。近年、邵中教授はブロックチェーンセキュリティに注力し、形式的検証技術をスマートコントラクトやオンチェーンプロトコルの安全保障に導入し、暗号資産の安全性に強力なサポートを提供しています。

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

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