Sonic Labs、DAGコンセンサスプロトコル向け形式検証ライブラリを発表

高性能レイヤー1ブロックチェーンSonicの背後にあるチーム、 ソニックラボ DAGベースのコンセンサスプロトコルのセキュリティ強化を目的とした形式検証ライブラリを発表しました。チーフリサーチオフィサーのベルンハルト・ショルツ博士が率いるこのライブラリは、Sonic独自のEVM互換ネットワークを含む、有向非巡回グラフ（DAG）ブロックチェーンの安全性を数学的に証明することを目的としています。

シドニー大学とINRIAの研究者との共同開発によるこのオープンソースライブラリは、TLA+証明支援技術を用いて構築されています。モジュール式で再利用可能なフレームワークを提供し、DAGアーキテクチャに基づくコンセンサスメカニズムのモデリングと検証のプロセスを効率化します。

この検証ライブラリは、DAG-Rider、Cordial Miner、Bullshark、Hashgraph、Alephといった既存のDAGベースのプロトコルの形式的証明を備えています。Sonic独自のプロトコルも、このフレームワーク内で派生として検証されています。この研究は、2025月11日から13日までバージニア州ウィリアムズバーグで開催されたNASA Formal Methods XNUMXカンファレンスで初めて発表され、ブロックチェーン検証標準における注目すべき進歩を示しています。

「ブロックチェーンにおけるセキュリティ上の欠陥は、手遅れになるまで検証されない仮定に起因することが多い」と、ソニックラボの最高研究責任者であるベルンハルト・ショルツ博士は声明で述べた。「このライブラリによって、私たちは希望から証明へと転換し、プロトコルがあらゆる状況下で安全に動作することを数学的な確実性をもって検証するためのツールを提供します。私たちの目標は、すべてのプロトコル開発者が形式検証を利用できるようにすることです」と、ショルツ博士は付け加えた。

ブロックチェーンの価値が急上昇する中、Sonic Labsはプロトコルのセキュリティと信頼性を確保するための形式検証フレームワークを発表

ブロックチェーンネットワークによって担保される価値が増大するにつれ、コンセンサスプロトコルの脆弱性がもたらす潜在的な影響はますます大きくなり、二重支払いや台帳状態の不整合といったリスクが生じています。従来のテストやコード監査では、バグのないシステムを保証する能力に限界があります。これに対し、形式検証手法が採用されています。 ソニックラボ 数学的証明を利用して、あらゆる可能性のある条件にわたってプロトコルのセキュリティを確認します。

このアプローチは、既存のコンセンサスプロトコルを検証するだけでなく、有向非巡回グラフ（DAG）ベースの新しいモデルを設計したり、既存のモデルを適応させたりする開発者にも役立ちます。この手法は現在、Sonicブロックチェーンが安全でない動作を示さないことを正式に検証するために実装されており、数学的検証を通じてプロトコルの信頼性を確立しています。

このイニシアチブは、検証ライブラリをオープンに公開することで、ブロックチェーン開発者に証明可能セキュアなシステムを構築するためのリソースを提供します。これにより、分散型エコシステム全体のレジリエンスが向上し、コンセンサスプロトコル検証に通常伴うリソース需要が削減されることが期待されます。