Web3 Scholars Summitで、イェール大学教授がLiDOモデルを初めて公開

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

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

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

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

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

邵中教授と彼のチームが以前開発したCertiKOSは、世界初の形式的検証を通じて「脆弱性のない」オペレーティングシステムであり、「ネットワーク物理システムの安全性のマイルストーン」と称賛されています。この成果は、彼らのシステムセキュリティ分野における深い蓄積を確立するだけでなく、この分野における専門能力を示しています。近年、邵中教授はブロックチェーンの安全性を深く研究し、2017年に彼の学生である顧荣辉教授と共に形式的検証技術をスマートコントラクトとオンチェーンプロトコルの安全保障分野に導入し、数千億ドル規模の暗号資産に安全保護を提供しました。

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