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

2025年Web3学者サミットが本日開催され、イェール大学のコンピュータサイエンス学科の教授、邵中が基調講演を行い、彼のチームが開発した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企業とエコシステムの長期的な発展戦略をより良くサポートすることを目指しています。

邵中教授は講演の最後に強調しました："信頼でき、安全で、検証可能なネットワークプロトコルスタックは、真の分散型未来への重要な道筋となるでしょう。"

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