Web3学者サミットは新しいコンセンサスプロトコルの安全検証フレームワークに焦点を当てています

最近開催された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の開発リーダーである邵中教授とそのチームは、システムセキュリティ分野で深い技術力を蓄積してきました。この成果は、彼らの今後の研究に堅固な基盤を提供するだけでなく、システムセキュリティ分野における卓越した貢献を示しています。近年、邵中教授は研究の重点をブロックチェーンセキュリティに移し、形式的検証技術をスマートコントラクトおよびチェーン上プロトコルの安全保障に応用することに取り組んでおり、数十億ドル規模の暗号資産に安全保護を提供しています。

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