# Web3学者峰会はコンセンサスプロトコルの安全性と活性証明に焦点を当てています2025年のWeb3学者サミットで、有名なコンピュータサイエンスの教授が「細化されたコンセンサスプロトコルの安全性と活性証明:LiDOとその拡張」というテーマで基調講演を行い、初めて彼のチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを公開しました。この画期的な成果は、複雑なビザンチン耐障害(BFT)コンセンサスプロトコルに対して機械的に検証可能な安全性と活性証明を提供することを目的としており、Web3エコシステムの信頼性とスケーラブルな発展のための技術的基盤を築くものです。! [CertiKの共同創設者であるShao Zhong教授は、Web3 Scholars Summitに出席し、LiDOモデルを初めて公開しました](https://img-cdn.gateio.im/social/moments-7f2809cd995635c37c41f88a101d02b1)講演者は、既存のコンセンサスプロトコル(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企業とエコシステムの長期的な発展戦略をより良くサポートすることを目指しています。講演の最後に、その教授は強調しました:"信頼でき、安全で、検証可能なネットワークプロトコルスタックは、真の分散型未来への重要な道筋となるでしょう。"この見解は、出席した学者たちの広範な議論を引き起こし、Web3技術の未来発展の方向性を示しました。
画期的なLiDOモデル:Web3コンセンサスプロトコルに機械的な安全性検証を提供
Web3学者峰会はコンセンサスプロトコルの安全性と活性証明に焦点を当てています
2025年のWeb3学者サミットで、有名なコンピュータサイエンスの教授が「細化されたコンセンサスプロトコルの安全性と活性証明:LiDOとその拡張」というテーマで基調講演を行い、初めて彼のチームが開発したLiDOモデルとLiDO-DAG拡張フレームワークを公開しました。この画期的な成果は、複雑なビザンチン耐障害(BFT)コンセンサスプロトコルに対して機械的に検証可能な安全性と活性証明を提供することを目的としており、Web3エコシステムの信頼性とスケーラブルな発展のための技術的基盤を築くものです。
! CertiKの共同創設者であるShao Zhong教授は、Web3 Scholars Summitに出席し、LiDOモデルを初めて公開しました
講演者は、既存のコンセンサスプロトコル(PBFTやJolteonなど)が広く使用されているものの、実装が複雑なために潜在的な脆弱性が隠れていることを指摘しました。この問題を解決するために、LiDOモデルは革新的に三層の詳細な検証フレームワークを提案しました:
現在、LiDOは産業級プロトコルJolteon(二段階BFT)および複数のDAGプロトコルに成功裏に適用され、1万行を超えるCoqコードの機械的証明を完了し、安全性と活性の検証コードはそれぞれ4000行と1700行に達しています。講演者は強調しました:"現在、PoSコンセンサスプロトコルは、安全性、活性、および分散化の三者を同時に満たすことが難しいというジレンマに直面しています。LiDOモデルは、このジレンマを打破するために提案された体系的な設計方案です。"
この教授が以前率いたチームが開発したCertiKOSは、世界初の形式的検証を通じて"脆弱性のない"オペレーティングシステムであり、"ネットワーク物理システムの安全におけるマイルストーン"と称されています。この成果は、彼のシステムセキュリティ分野における深い蓄積を確立しただけでなく、その後の研究に重要な基盤を提供しました。
LiDOは現在、モデル設計と形式化検証を完了し、主流のパブリックチェーンおよび分散型プロトコルとの統合の可能性を探り始めています。講演者は、Web3.0における重要なメカニズムの検証に取り組んでおり、全周期の製品とサービスを提供し、Web3企業とエコシステムの長期的な発展戦略をより良くサポートすることを目指しています。
講演の最後に、その教授は強調しました:"信頼でき、安全で、検証可能なネットワークプロトコルスタックは、真の分散型未来への重要な道筋となるでしょう。"この見解は、出席した学者たちの広範な議論を引き起こし、Web3技術の未来発展の方向性を示しました。