Steelhead: Interleaving Partially Synchronous and Asynchronous Commit Rules on a Shared DAG
Zeno De Angeli, Philipp Jovanovic, Lefteris Kokoris-Kogias, Markus Legner, Alberto Sonnino
cs.DC
Sep 24, 2026 · v2
cs.CR
TL;DR
Safety and liveness of the Steelhead dual-mode DAG consensus protocol are machine-checked with mechanized proofs in Lean 4.
Abstract
Dual-mode consensus protocols are fast when the network is partially synchronous and remain live under asynchrony. We introduce Steelhead, a dual-mode mechanism that composes a partially synchronous and an asynchronous commit rule over one DAG: every k-th round is decided by the asynchronous rule, whose leader a common coin reveals after the votes, and all other rounds by the partially synchronous rule. Every interval, validators replay the committed DAG under each candidate period, adopt the one with the fewest expected message delays, and fall back to k = 1 when the output stalls; the asynchronous rule applied to the coin rounds alone keeps the protocol live. Steelhead sends no message beyond the DAG's blocks, not even to agree on the period, and opens a coin only on the rounds that need a hidden leader. It is generic over pairs of DAG commit rules that share a committee; we instantiate it with Mysticeti and Mahi-Mahi at n >= 3f+1 and with the two variants of BlueBottle at n >= 5f+1. We prove it safe and live, and provide mechanized proofs in Lean 4. In simulation, Steelhead matches the partially synchronous protocol in a healthy network, stays close to the asynchronous one when network conditions stall the partially synchronous one, and adapts quickly in both directions.
Problem
Dual-mode BFT consensus protocols aim to be fast under partial synchrony while staying live under asynchrony, but existing designs pay a cost for the mode-switch decision (timeouts, reconciliation, extra agreement rounds, or a coin per wave).
Approach
Steelhead composes a partially synchronous and an asynchronous commit rule over a single shared DAG, using the round number to select which rule decides each slot: every k-th round is decided by the asynchronous rule via a common coin, and others by the partially synchronous rule. The period k is adapted at runtime by replaying the committed DAG under candidate periods and choosing the one with fewest expected message delays, falling back to k=1 when stalled. Safety and liveness are proven for any pair of rules meeting an interface, with the proofs machine-checked in Lean 4.
Results
Steelhead is proven safe and live in Lean 4 and instantiated with Mysticeti/Mahi-Mahi (n>=3f+1) and BlueBottle variants (n>=5f+1). In simulation it matches the partially synchronous protocol in healthy networks, stays close to the asynchronous one when the fast path stalls, and adapts promptly in both directions.
| Statement | Lean result | Content |
|---|
| Lemma 1 | Safety | Directly skipped slot has no certificate; two certified candidates of one author/round coincide |
| Lemma 2 | Safety | Directly committed candidate is certified in causal history of every block at round r+w |
| Theorem 0.B.1 | Safety, Interface | Two views deciding agree |
Lean-verified safety results
