Web3学者峰会上邵中教授发布LiDOモデル，推進コンセンサスプロトコルの安全性検証

2025年Web3学者峰会近日举行，耶鲁大学計算機科学系教授邵中が「基于细化的コンセンサスプロトコル安全性与活性证明：LiDO及其拓展」というテーマの講演を行いました。彼は初めて、彼のチームが開発したLiDOモデルおよびLiDO-DAG拡張フレームワークを公開しました。この画期的な成果は、複雑なビザンチン耐障害（BFT）コンセンサスプロトコルに対して、機械的検証可能な安全性と活性の証明を提供し、Web3エコシステムの信頼性とスケーラブルな発展のための技術基盤を築くことを目的としています。

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

邵中教授は講演の中で、既存のコンセンサスプロトコルである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企業とエコシステムの長期的な発展戦略をより良くサポートすることを目指しています。講演の最後に、邵中教授は次のように強調しました："信頼でき、安全で、検証可能なネットワークプロトコルスタックが、真の分散型未来への重要な道筋となるでしょう。"