This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
イェール大学の教授が初めてLiDOモデルを明らかにしました：BFTコンセンサスプロトコルに機械的検証を提供する
Web3学者サミットでイェール大学教授が初めてLiDOモデルを公開
最近開催された2025年Web3学者サミットで、イェール大学コンピュータサイエンス学科の教授である邵中氏が「細化に基づく合意プロトコルの安全性と活性証明：LiDOおよびその拡張」というタイトルの基調講演を行い、彼のチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを初めて明らかにしました。この革新的な成果は、複雑なビザンチン耐障害（BFT）合意プロトコルに対して機械的に検証可能な安全性と活性証明を提供することを目的としており、Web3エコシステムの信頼性と大規模な発展のための技術基盤を築くことを目指しています。
邵中教授は講演の中で、既存のコンセンサスプロトコル（PBFTやJolteonなど）が広く使用されているにもかかわらず、実装の複雑さから潜在的な脆弱性が隠れていることを指摘しました。この問題を解決するために、LiDOモデルは革新的に三層の詳細な検証フレームワークを提案しました。
現在、LiDOは産業グレードのプロトコルJolteon（二段階BFT）および複数のDAGプロトコルに成功裏に適用され、10,000行を超えるCoqコードの機械的証明を完了しました。その中で、安全性と活性の検証におけるコード量はそれぞれ4,000行と1,700行に達しています。邵中教授は講演の中で次のように強調しました："現在、PoSコンセンサスプロトコルは、安全性、活性、分散化の三者を兼ね備えることが難しいという課題に直面しています。LiDOモデルは、この困難を突破するために提案された体系的な解決策です。"
邵中教授が率いるチームは、CertiKOSを開発しました。これは、形式的検証を通じて作られた世界初の「バグのない」オペレーティングシステムであり、「サイバー物理システムの安全性におけるマイルストーン」と称されています。この成果は、彼らがシステムセキュリティの分野で築いた堅固な基盤を示すだけでなく、その分野における豊富な経験も示しています。近年、邵中教授はブロックチェーンセキュリティの研究に専念しており、2017年に同僚と共にセキュリティ会社を設立し、形式的検証技術をスマートコントラクトやオンチェーンプロトコルのセキュリティ保証に導入しました。これにより、価値千億ドルの暗号資産に対する安全保護が提供されています。
! CertiKの共同創設者であるShao Zhong教授は、Web3 Scholars Summitに出席し、LiDOモデルを初めて公開しました
LiDOは現在、モデル設計と形式的検証を完了し、主流のパブリックブロックチェーンおよび分散型プロトコルとの統合の可能性を探り始めています。邵中教授は、Web3.0における重要なメカニズムの検証に取り組んでおり、全周期の製品とサービスを提供し、Web3企業およびエコシステムの長期的な発展戦略をより良くサポートすることを目指しています。講演の最後に、邵中教授は次のように強調しました："信頼でき、安全で、検証可能なネットワークプロトコルスタックは、本当の分散型未来への重要な道筋となるでしょう。"