← All papers
First page of Hydrozoan: Latency-Adaptive DAG Consensus under Mixed Byzantine and Crash Faults

Hydrozoan: Latency-Adaptive DAG Consensus under Mixed Byzantine and Crash Faults

Qianyu Yu, Lefteris Kokoris-Kogias, Alberto Sonnino

cs.DC Sep 22, 2026 · v1 cs.CR
Safety and liveness of the Hydrozoan and Optimal-Hydrozoan DAG consensus protocols are machine-checked in Lean 4 on top of Mathlib.
DAG-based consensus protocols can achieve great throughput and the optimal three-message-delay limit for n = 3f+1 consensus. While two-delay protocols exist, they pay with reduced resilience (requiring 5f+1-style committees) or rely on fallbacks that sacrifice the DAG's high throughput. This paper introduces Hydrozoan, the first DAG protocol with a dual commit path under a hybrid fault model of f Byzantine and c crashed validators, on n = 3f+c+2p+1 validators. Leaders commit in two message delays whenever at most p validators are faulty, and in three otherwise, with no extra messages, no view changes, and multiple leaders per round. Both paths are evaluated on the same DAG, using a novel graded indirect rule to reconcile them so that every honest validator reaches the same decision. We show that under geo-distributed conditions, which path is faster is a property of geography rather than the protocol, as rounds reaching a remote region cost far more than those that do not. The (f, c, p) knobs place the fast quorum where the deployment requires it, allowing a commit in two message delays. If misconfigured, Hydrozoan can still commit in three message delays: Hydrozoan commits on whichever path fires first. We also present Optimal-Hydrozoan, a variant that tolerates one more fault on the fast path, the first construction to match the known lower bound. The safety and liveness of both protocols are machine-checked in Lean 4. Our geo-distributed evaluation shows that Hydrozoan matches Mysticeti's throughput, commits 25% faster when the fast quorum fits fast regions, and falls back to three message delays when it does not or past p faults, where existing two-delay protocols stall.

DAG-based Byzantine consensus protocols either achieve three-message-delay commits at n=3f+1 or pay with larger committees or fallbacks to reach two-delay commits. A tunable dual-path protocol handling mixed Byzantine and crash faults with proven correctness is lacking.

Hydrozoan runs on an uncertified DAG (like Mysticeti) with a hybrid fault model of f Byzantine and c crash faults on n=3f+c+2p+1 validators. Votes are edges, so both a fast quorum path and a direct certificate path are read off the same blocks. A graded indirect rule reconciles paths so all honest validators decide identically. All lemmas for both Hydrozoan and Optimal-Hydrozoan are machine-checked in Lean 4 on Mathlib, with no sorry and only Lean's three standard axioms.

Hydrozoan matches Mysticeti's throughput, commits about 25% faster when the fast quorum fits fast regions, and falls back to three message delays otherwise instead of stalling. Optimal-Hydrozoan is the first construction to match the known lower bound, tolerating one more fault on the fast path.

ProtocolnDelaysMulti-leaderDAGMachine-checked
Mysticeti3f+13yesuncertifiedyes
Hydrangea3f+c+2p+12/3nonono
Hydrozoan3f+c+2p+12/3yesuncertifiedyes
Optimal-Hydrozoan3f+c+2p-12/3yesuncertifiedyes
Protocol comparison (delays, faults, machine-checked)