CertiK共同創業者の邵中教授がWeb3学者サミットに出席し、初めてLiDOモデルを公開しました。

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

本日開催されたWeb3 Scholars Conference 2025では、イェール大学コンピュータサイエンス学部の教授であり、CertiKの共同創設者であるShao Zhong氏が「Proof of Security and Activity of Consensus Protocols Based on Refinement: LiDO and Its Extensions」と題した基調講演を行い、彼のチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを初めて公開しました。 この画期的な成果は、複雑なビザンチンフォールトトレランス(BFT)コンセンサスプロトコルのセキュリティと活性の機械的に検証可能な証明を提供し、Web3エコシステムの信頼性と大規模開発のための技術的基盤を築くことを目的としています。

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

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

現在、LiDOは産業レベルのプロトコルJolteon（二段階BFT）や複数のDAGプロトコルに成功裏に適用され、1万行を超えるCoqコードの機械的証明を完了し、安全性と活性の検証コードはそれぞれ4000行と1700行に達しています。「現在、PoSコンセンサスプロトコルは安全性、活性、分散化の三つを同時に達成することが難しいというジレンマに直面しています。」と邵中教授は講演で指摘しました。「LiDOモデルはまさにこのジレンマを打破するために提案された体系的な設計方案です。」

Shao Zhong教授率いるチームによって開発されたCertiKOSは、世界で初めて正式な検証に合格した「脆弱性のない」オペレーティングシステムであり、「サイバーフィジカルシステムセキュリティのマイルストーン」として知られています。 この成果は、セキュリティ企業であるCertiKの技術の基礎を築くだけでなく、システムセキュリティの分野での深い経験を示すものでもあります。 近年、Shao Zhong教授はブロックチェーンセキュリティに深く関与しており、2017年に弟子のGu Ronghui教授とCertiKを共同設立し、スマートコントラクトとオンチェーンプロトコルのセキュリティに形式検証技術を導入し、数千億ドルの暗号資産のセキュリティを護衛しています。

現在、LiDOはモデル設計と形式検証を完了し、主流のパブリックチェーンや分散型プロトコルとの統合の可能性を模索し始めています。 Shao Zhong教授は、CertiKはWeb3.0の主要なメカニズムを検証し、Web3企業とエコシステムの長期的な開発戦略をよりよくサポートするためのフルサイクルの製品とサービスを提供することに取り組んでいると述べました。 講演の最後に、Shao Zhong教授は「信頼性が高く、安全で、検証可能なネットワークプロトコルスタックは、真に分散化された未来への重要な道筋となるでしょう。 ”