要点 - 新しいデュアルモード合意方式「Steelhead」は、1つのDAG（有向非巡回グラフ）上で部分同期型と非同期型のコミット規則を交互に適用することで、「ネットワークが良好なときは高速に進み、停滞や遅延が起きたときにもライブネス（進行性）を保つ」ことを目指している。 - 著者らは形式的な安全性・ライブネスの証明を与え、Lean 4による機械化証明も示している。シミュレーションでは部分同期プロトコルと同等の性能を出しつつ、停滞時には非同期プロトコルに近い振る舞いで継続することを確認している（arXiv:2609.30163v1）。

概観（平易な説明） 分散合意の世界では「部分同期モデル」と「完全非同期モデル」が代表的な理論モデルです。前者は適度な通信遅延の上限が存在することを仮定して速い決定を可能にする一方、遅延上限が破られると動作が停滞することがあります。後者は遅延に対して頑健で常にライブであるが、通常はよりコストが高かったり遅めになりがちです。

Steelheadは、DAG（トランザクションや投票を木ではなくネットワーク状に重ねる構造）という単一のデータ構造の上で、ある周期性（毎k回のラウンド）に応じて「非同期ルール」を使うラウンドを挟み、それ以外のラウンドでは部分同期ルールを使う仕組みです。非同期ラウンドでは共通コイン（leaderを隠すための乱数）を用いて決定を引き起こし、これによりネットワーク条件が悪化してもプロトコルが止まらないようにしています。

設計の特徴と強み - 1つのDAGだけを用いる点：別途同期用のメッセージを送る必要がなく、追加の合意フェーズを設けないため設計がシンプルに保たれている。論文によれば、DAGのブロック以外に新たなメッセージを追加で送らない点が特徴。 - コインやリーダーの出現は必要なラウンドだけに限定：毎k回だけコインを開き、他は部分同期ルールで高速決定を狙う。さらに合意の出力が停滞した場合はkを1に落として即座に非同期ルールを常時使えるように切り替えるなど、適応的な振る舞いをする。 - 汎用的な構成：共通の委員会（validators）を共有できる限り、複数のDAGコミット規則の組合せに対して一般的に適用できる設計になっている。論文では具体例として Mysticeti と Mahi-Mahi（n >= 3f+1）や BlueBottle の2変種（n >= 5f+1）に対する実装を示す。

理論面と機械化証明 著者らは安全性とライブネスについて理論的に証明しており、さらにLean 4を用いた機械化証明も付けている点は注目に値します。機械的検証があることで、理論上の主張が人間のミスによる穴をある程度減らしていることが期待できます。

評価（シミュレーション結果） 論文中のシミュレーションでは、正常で良好なネットワークでは部分同期型のプロトコルとほぼ同等のスループットを示し、部分同期側が停滞した条件下では非同期側に近い性能を保つことが示されています。切り替えの適応性も短時間で効くことが観察されています。

注意点と限界（慎重な見方） - モデル上の仮定：安全性・ライブネスの証明や閾値（n >= 3f+1やn >= 5f+1）は数学的モデルと攻撃モデルの下で成り立ちます。実運用環境の複雑なネットワーク特性や実装上の脆弱性が結果に影響する可能性は残ります。 - 実証の程度：シミュレーションは有益ですが、実ネットワーク・長期運用・悪意ある複合攻撃下での挙動はさらに検証が必要です。特に共通コインの実装方法やランダム性、DAGの運用コスト、遅延や帯域に対する実装上のオーバーヘッドなどは実験的に確かめる必要があります。 - 複雑さと運用の現実性：k の動的調整やDAGの再生（replay）を各バリデータが行う設計は理論的には正しいとしても、実装や運用における複雑さ・最適化課題が残ります。