Rohu-Paplet: Fast Finality That Survives Recovery

Fast consensus protocols finalize a block in two message delays when the network behaves. When it does not, a timer fires and recovery takes over. Rohu-Paplet is an idea about the awkward moment in between.

A timeout does not erase votes. Validators may already have signed enough PREPAREs to form a fast certificate. A Byzantine collector can hold that certificate back and show it after recovery picks something else. If recovery is careless, the chain now has two certified children.

The late-certificate problem. Recovery must preserve what could already finalize, not only what its participants have seen. Here f = 1 and n = 6, and a Byzantine collector holds FAST(x) back past a timeout. In B, each closed status carries its author’s own PREPARE. At least 2f+1 = 3 honest statuses in S_p report x, so protect(S_p) = x and the first valid resolution certifies x. The revealed FAST is a second proof of the same child.

So recovery cannot read only what its participants have seen. It has to read what could already finalize. This post explains how Rohu-Paplet does that with one counting argument, one closable domain per block, and an ordering service that never stops. It builds on BlueBottle, Hydrozoan, FinWhale, Alpenglow, and Cordial Miners. What it adds is a fast path per parent, kept beside an asynchronous DAG that only orders recovery outcomes.

The names come from two fish. The rohu lives in rivers, and here it is River, the fast path. The paplet lives in the sea, and here it is Ocean, the asynchronous ordering service.

Two routes, one order

Rohu-Paplet runs both routes all the time. River tries to finalize the next block directly. Ocean keeps ordering control records in the background, whatever River is doing.

Dependencies of finality. Ocean supplies accepted cuts and orders recovery records continuously. Only a valid finality route authorizes a child. Redrawn from the TikZ source in paper4/overview.tex.

Both routes authorize the same kind of object: an exact child of a certified parent. A child that River certifies and the same child that Ocean certifies are one child. The application follows the chain of certified parents and never asks which route supplied the proof.

Ocean has two jobs. It supplies accepted cuts of its DAG, which say which transaction data a new child includes. It also orders recovery records for blocks that stall. Neither job lets Ocean choose the next block by itself.

One counting argument

The committee has n = 5f+1 validators, and at most f of them misbehave over the whole run. Every safety argument here uses one fact about overlaps between two sets of validators:

| A \cap B | \geq | A | + | B | - n

Lemma (unique prepare protection). The signer sets of any U and any FAST for the same parent domain share at least one honest validator, and an honest validator never prepares two children in one domain. FIN inherits the same uniqueness through the complete U it retains.

Two sets of 3f+1 share at least f+1 validators, so at least one honest one. A set of 4f+1 and a set of 3f+1 share 2f+1. Two sets of 4f+1 share 3f+1, so at least 2f+1 honest ones. An honest validator never signs two conflicting values for the same block, so these overlaps force agreement.

The protocol uses four sizes. A fast certificate, FAST, takes 4f+1 PREPAREs. A protection certificate, U, takes 3f+1 PREPAREs. A receipt certificate, FIN, takes 2f+1 receipts, and a closure set takes 4f+1 closed statuses.

River, the fast path

Each certified block p gets exactly one fast attempt at its child. The leader for that height proposes a child x with all its evidence. Each open validator checks it, saves its choice to disk, and sends one PREPARE.

Fast-path message sequence. The validator lane stands for the honest quorum and its internal multicast exchange. Each included observer has the complete proposal evidence. Dissemination through a collector only has a different observer latency. Redrawn from paper4/river.tex.

An observer that sees 4f+1 matching PREPAREs has FAST and finalizes x after two message delays. A validator that holds a complete U for x can also send a receipt. With 2f+1 receipts, an observer has FIN one delay later.

FIN needs fewer signatures, but its strength comes from somewhere else. Every receipt signer holds the complete U. That retained U is what recovery finds later.

A validator writes each choice to durable storage before it releases the signature. After a restart, it restores those choices before it signs again. Forgetting a vote that is already out is how forks start.

One validator’s durable entry for d_p. The PREPARE choice and the receipt are one-shot slots. Each signature is persisted before it is released. Closure freezes both slots and publishes an immutable status with the author’s own PREPARE and every retained complete U. Learning FAST or FIN stays legal in either state and enables d_x.

When the fast path stalls

River has no view change. If the child of p does not finalize in time, a local timer closes the domain of p. A closed validator never signs another PREPARE or receipt for a child of p.

Closure publishes a closed status. The status carries the validator's own PREPARE, if it sent one, and every complete U it kept. Seeing f+1 closed statuses also makes a validator close, so closure spreads.

Parent-local recovery. Closure, status collection, and ordered resolution are three separate functions. A status set alone is preservation evidence, not an agreement decision. The first-valid-record rule of Ocean supplies agreement.

Any validator can collect 4f+1 closed statuses into a set S. One rule reads the set, and the first matching line wins:

protect (S) = x

if S contains a complete U for x

protect (S) = x

else, if at least 2f+1 statuses in S report their own PREPARE for x

protect (S) = ⊥

otherwise: this set forces no child

A resolution record carries the parent with its proof, the set S, and a fallback child for the case where the rule returns ⊥. Ocean orders these records. The first valid record for p in Ocean order certifies its child, and later records for p change nothing.

Why a hidden certificate survives

Suppose a FAST for x exists, but nobody in recovery has seen it. Its 4f+1 signers and the 4f+1 status authors overlap in at least 3f+1 validators. At most f are faulty, so at least 2f+1 honest validators appear in both.

Why a hidden final survives closure. Top: a FAST and a closure set S share at least 2(4f+1) − n = 3f+1 signers, so at least 2f+1 honest signers report their own PREPARE(x). Bottom: a FIN has at least f+1 honest receipt signers, and only f identities lie outside S. So at least one honest holder of the complete U_p(x) reports inside S. Neither case needs anyone in S to have seen the final certificate.

Each of those honest validators signed its PREPARE for x before it closed, because closing forbids new signatures. So each of their statuses reports a PREPARE for x, and the second line of the rule selects x. A hidden FIN works the same way: some honest receipt signer is in S and shows its U.

When no certificate exists, two valid closure sets can disagree, and that is fine. Every valid set keeps any child that could already finalize. Ocean's first-record rule picks one answer among the rest.

The receipt threshold is tight for this kind of rule. With 2f receipts instead of 2f+1, two executions can give identical statuses while they hide conflicting finals.

Why the receipt threshold is 2f+1 for this interface. The partition is not to scale. A Byzantine leader signs two valid successors x and y. A prepares x and C prepares y in both executions, and T switches between them. Cross-group PREPAREs, every complete U, every receipt, and every vote from T reach S only after the recovery decision. So the 4f+1 reporters in S sign identical statuses in E_x and E_y, while the weakened finals conflict. At 2f+1 receipts, at least one honest holder must lie inside S. Source: paper4/receipt_bound.tex.

One domain per block

Recovery closes one domain: the successor domain of one certified block. The domain name is a hash of the block's semantic identity, and that identity leaves out signatures and proof bytes. So two proofs for the same block open the same domain.

This matters once descendants run ahead. Say an observer learned FAST for x and already certified a child y of x. A late resolution of p must certify exactly x. It cannot add a recovery block after x, because that block would compete with y.

Exact parent domains. Closing d_p changes only the entry for d_p, so d_x stays open and y stays certified. A late resolution of p is one more proof of the same x. It cannot append a recovery transition after x. Its proof bytes cannot open a second domain for x, because id(x) excludes proof representations.

Closing the domain of p never touches the domain of x. The old parent stays closed forever, and the chain continues from its certified child. There is no global stop and no checkpoint ceremony.

Where the transactions come from

Producers run their own chains of transaction blocks in parallel. A block becomes usable when 3f+1 validators sign that they hold it, which makes a DA certificate. At least 2f+1 of those holders are honest, so the data stays retrievable.

A child names an accepted cut of the Ocean DAG. Each producer's position moves to the highest certified block that the cut advertises. Sweep then sorts the new blocks by sequence, producer index, and digest, so every validator derives the same ordered delta.

Producer chains to one ordered delta. Each producer keeps an append-only chain. A frontier gives one certified position per producer. The child frontier is the coordinatewise maximum of the parent frontier and every compatible DA-certified coordinate advertised in the complete source cut. Sweep then orders the newly included blocks deterministically.

An earlier version taught us that this frontier cannot be guessed. For f ≥ 2, no rule over a node's local cone alone can carry fast extensions both completely and soundly. So the frontier travels as a signed artifact, and each child commits to it.

Ocean, the part that never stops

Ocean is a DAG of control vertices, built round by round with reliable broadcast. Each vertex needs at least 4f+1 parents from the previous round. Rounds advance even when vertices carry no transactions, so recovery never waits on data.

Two delivery routes, one payload. An honest validator persists one ECHO and one READY per slot before it sends them, and every ECHO holder keeps the body. READY fires on E = 3f+1 ECHOs of one digest or on f+1 READYs. READY relay does not wait for the payload. Fast delivery needs F = 4f+1 ECHOs. Slow delivery needs 2f+1 READYs. At most one payload per slot can have either proof.

Broadcast has two delivery routes. The fast route needs 4f+1 ECHOs of the payload, and the slow route needs 2f+1 READYs. Either way, at most one payload per slot delivers, and every honest node eventually gets it.

Ocean groups rounds into waves and elects one leader vertex per wave with a common coin. Before an honest validator releases its coin share, it fixes a seal of the wave. Every seal contains a common core of at least Q = 4f+1 candidates.

One Ocean wave at f = 1. Each vertex has Q = 4f+1 = 5 strong parents, k = ⌈log₂ Q⌉ = 3, and the wave length is W = k+2 = 5 rounds. Faint edges are strong parent references. The dashed circle is the missing slot of a silent author. Pairing the five sealed endpoints k times gives one second-round common ancestor, and its Q first-round parents form the core. The coin is uniform over n authors, so an eligible wave hits the core with probability at least Q/n.

The coin hits the core with probability at least Q/n. Under an ideal-coin assumption, a miss gets unlikely quickly:

\Pr [no hit in t waves] \leq {(f / n)}^{t}

each eligible wave misses with probability at most f/n

E [waves to a hit] \leq \frac{n}{Q} = \frac{5 f + 1}{4 f + 1} < \frac{5}{4}

a count of waves, not seconds

These bounds count waves. Real time still depends on the network.

What it costs

With ready evidence and a one-way delay of at most δ, FAST forms at 2δ and FIN at 3δ. Fresh data takes longer: 2δ for its DA certificate, 2δ for an accepted cut, and 2δ to ratify. That is 6δ from dissemination.

Where the delays go. Row 1: fresh data can need 2δ for its DA certificate, 2δ for an accepted advertised cut, and 2δ for ratification. Row 2: a proposal with complete evidence reaches FAST at s + 2δ. The receipt route needs one more leg, so a freshly built FIN forms at s + 3δ. Row 3: after warmup, consecutive eligible honest leaders can overlap accepted-cut production and decide every 2δ, if each turn has a fresh, strictly later cut and complete evidence ready. All rows assume ready prerequisites, one-way delay at most δ, and signers that stay open. Processing and persistence are inside the δ envelope or charged separately.

Messages are not cheap. PREPAREs go all to all, which is O(n²) transmissions per block. Each broadcast slot is O(n²) messages, so one Ocean round is O(n³). A stalled block costs one ordered resolution, which counts stages, not time.

An early timeout can also cut off an honest proposal that was about to finalize. Safety survives, because recovery keeps anything that could finalize. Speed does not, so timers back off: T_j = min(2^j·T₀, T_max).

Two fewer validators, no reliable broadcast

The 5f+1 comes from the recovery rule, not from the problem. The rule above counts reports and ignores who wrote them. A rule that reads authors needs fewer validators. One inequality says how many.

2 q_{F} + q_{S} \geq 2 n + 2 f + c

Where the two validators go. Each recovery rule fits one value of c in the inequality. Counting reports without authors needs 5f+1. Reading the leader's signature from each PREPARE needs 5f. Setting aside a leader caught signing two children, then waiting for one more status, needs 5f−1. Kuznetsov, Tonkikh, and Zhang proved that 5f−1 is the floor for two-step consensus.

Here q_F is the fast quorum and q_S the number of closed statuses. Both are at most n − f, or recovery could wait forever. At n = 5f−1, FAST needs 4f−1 PREPAREs, U needs 3f, and FIN needs 2f receipts.

The exclusion step comes from Kuznetsov, Tonkikh, and Zhang. Two leader-signed children prove the leader is faulty. Recovery drops the leader's status, waits for one more, and selects a child with at least 2f own PREPAREs. An exhaustive search for f up to 5 found no status set where this rule loses a late FAST.

Ocean drops reliable broadcast at the same time. It runs on an uncertified DAG, where each vertex goes once to each validator. Its commit rule is the asynchronous rule of Cordial Miners, with five-round waves and quorums of 4f−1. One round costs n(n−1) messages instead of 3n²(n−1).

One push per vertex. With reliable broadcast, every vertex is echoed and relayed, so a round costs 3n²(n−1) messages. On an uncertified DAG each vertex goes once to each validator, so a round costs n(n−1), which is 3n times fewer. The benchmark matched the first formula exactly at n = 6 to 21. A simulation of the second adds 4 to 9 percent for fetches.

The price is speed. Each Ocean wave commits with probability at least (3f−1)/(5f−1), which is one half at f = 1. A good-case Ocean commit takes about 5δ instead of 4δ. The recovery bounds have hand proofs, and the Ocean rule has hand proofs and adversarial fuzzing for f up to 3. Nothing here is mechanized or peer reviewed yet.

Each piece exists somewhere already. BlueBottle runs an asynchronous uncertified DAG at 5f+1. FinWhale and Hydrozoan run 5f−1 fast paths on a DAG, but they are live only under partial synchrony. We found no published protocol with a two-delay fast path at 5f−1 that also stays live under full asynchrony. Rohu-Paplet at 5f−1 has both on paper. Storage and data availability carry over with smaller thresholds and one new rule for honest resolvers.

The chain reads the weather

No view change. No fallback subprotocol. No message that says the network is in a storm. In the weather-reading design, every validator writes one uncertified DAG the same way in every weather, and two readers interpret it. River reads it under partial synchrony, and Ocean reads it under asynchrony. The storm is evidence in the DAG, so every node finds the same switch point.

Two fish, one river. One uncertified DAG carries one wire format in every weather. River and Ocean interpret it under different synchrony assumptions. The flip and the heal move tenancy between them, and confluence (O1-C) collapses both readings into one order. The DAG is stylized: five authors per round, four parents each.

Votes live inside the blocks as flags. A strong(r) flag supports the round-r leader and promises never to cast ⊥(r), the vote to skip that leader. River reads three outcomes: with 4f+1 strong flags, the leader block finalizes at 2δ. A notarization plus 3f+1 fin flags finalizes it at 3δ, and 3f+1 ⊥ flags give a skip-cert, so the round never finalizes. Ocean runs waves of three rounds, and a threshold coin elects one anchor per wave. That anchor commits only with a BindCert of 3f+1 bindings.

A storm leaves a scent that no cone can hide. A monsoon starts with k_out consecutive skip-certs, the trigger, and those rounds can never finalize. A strong or fin flag is invalid if its cone shows at least f+1 distinct ⊥ authors in each of k_out consecutive rounds. A full skip-cert can hide from a cone, but that scent cannot. So each node leaves River on its own, by reading its own cone, with no message to anyone. Exit is unilateral because agreeing that a storm has started would need the consensus the storm just broke.

Coming back takes one ratified object, the Heal, which lifts the suppression for everyone at once. If each node re-entered on its own calm, two honest nodes could re-enter at different rounds and read different values. Calm seas are k_in consecutive post-flip rounds, more than k_out, each with a notarized leader and at most f distinct ⊥ authors. The Heal is the first committed Ocean anchor whose cone holds calm seas, and every cone carries it within two rounds. Nobody holds a referendum on rain, but when the trains restart, everyone hears the same announcement.

A monsoon, start to finish. Consecutive skip-certs on [x, x+k_out) form a trigger, and those rounds are finality-dead by L4. From x+k_out the forced scent suppresses river finality and Ocean is canonical. One ratified Heal at round h lifts the suppression by h+2. The dashed gap [h, h+2) can only produce fewer certificates, never extra ones.

Both readings give one sequence, and in the weather-reading design a machine checked that for all N. O1-C states that all honest observers deliver the same anchor sequence and transaction order. Nobody revises a delivered prefix. Both readings run all the time, because no rule over one cone can decide soundly and completely whether a storm is on. The design makes that question moot.

The 3δ slow path and Ocean are unconditionally safe against f Byzantine validators. The 2δ fast path is safe under granular synchrony, and the flip gates it for exactly the regime where that assumption fails. No proof, measurement, or build yet joins the weather layer with the parent-local recovery in this post.

Every block flips and heals on its own

The weather version flipped and healed the whole chain at once. The current design runs the same cycle for one block at a time. Each certified block p owns one signing domain, d_p, and gets one River attempt for its child. The cycle has three steps, and none of them changes another block's signing rights.

One block's weather. Domain d_p finalizes by FAST, and its child x opens d_x. A timeout closes d_x, the flip for that block alone. Ocean's first valid resolution over 4f+1 closed statuses picks child y, and certifying y opens d_y with no Heal record.

A closure is the flip. If d_p stalls, a local timer closes it at one validator, and that validator asks nobody. Any honest validator that receives f+1 closed statuses closes it too, and the Byzantine validators alone never reach f+1. Ocean's first valid resolution for p, built from exactly 4f+1 closed statuses, is the decision. The certified child is the heal, because it opens the next domain at once.

Each step is built so that it never has to prove a negative. A timeout cannot prove that an unseen FAST is absent, so the closure does not try. It only promises no new signatures, and each closed status carries its signer's own PREPARE and any complete U it holds. So if a FAST or FIN could still form, every valid status set selects its child. Proposals carry their parent's complete finality proof, so the anchor rule R3 is gone.

Three results finish the per-block weather. First, a storm mode: in a long storm, each block still waits out its full timer before it closes. A validator that learns of k_out resolved blocks in a row could close new domains at once, while fixed probe heights still try River. Second, a return theorem: after the network stabilizes, with the cap larger than the honest fast-path delay, each early honest closure raises its signer's floor. The theorem to prove is that this caps how many honest-leader blocks can miss FAST. Third, a leader rule could skip identities whose recent turns ended in a resolution, so repeated faulty leaders stop costing a full timer each.

Order is an artifact

Two planes, one seam. The control clock counts only control parents, so withholding on a data chain cannot stall it (T1). Producers disseminate in parallel under DA certificates of 3f+1 votes. A committed anchor and the certified tips it sees meet in one object, the FrontierCert, which records the frontier as a hash-linked artifact.

For f ≥ 2, no node can work out the frontier from its own cone, so the frontier travels as an artifact. The two-plane design runs the producer chains as a data plane below the control DAG. The control clock counts only control parents, so a producer that withholds data cannot stall it. The planes meet at one object, the FrontierCert.

Two executions prove it. A Byzantine producer signs two incompatible blocks, x and y, at one height. Both executions share one byte-identical cone, yet x gets a fast certificate in one and y in the other. The second execution needs two faulty validators, which is why the result starts at f = 2. At f = 1 the paper makes no claim.

Why the frontier must be carried, at f = 2. The seven-column cone is byte-identical in both runs. In E_x, the outside authors and two equivocators give x nine supporters. In E_y, the outside authors and one equivocator give y nine. No cone-local rule can pick the right branch in both.

A FrontierCert carries its round, the anchor's hash, its parent's hash, a Merkle root of the frontier, an evidence root, and its signers. Its evidence is a River fast pool of 4f+1 votes or a committed Ocean anchor, and any verifier recomputes the frontier from it. A valid FrontierCert never moves a chain's position backward. Candidates from different vote pools can differ, so the chain ratifies one, and later anchors descend from it.

Four obligations, T1 to T4, join the planes: a data-independent control clock, carried River frontiers, deterministic Ocean extraction, and one log with one checkpoint sequence. T1 and the candidate compatibility in T2 are machine-checked for all N, and T3 and T4 are hand proofs. Order must be an artifact, not an extraction.

Certificates you can hand to a stranger

A skip-cert is a thing you can hand to a stranger. In the weather-reading design, each vote rides in a signed block with its promise attached. So a certificate is a self-contained artifact, not a pattern in one observer's view. A ⊥(r) after its author's own strong(r) breaks a promise, and so does a fin without its strong. Two signed vertices prove either one, and a light client checks them without the DAG. Cordial Miners already treats signed equivocation as an accountable fault, so the new part is light-client portability.

Evidence you can hand over. In the weather-reading design, a strong(r) flag carries its author's promise never to cast ⊥(r). A ⊥(r) signed by the same author breaks that promise, and the two signed vertices are the whole proof. A light client checks it without holding the DAG. A fin without its strong has the same shape.

The two-plane design keeps this across both planes. Four header faults stay constant-size: a double control vote, ⊥ after own strong, fin without its prerequisite, and a double DA vote. A fault inside a vector vote needs Merkle openings, so its proof grows as O(log K) in the number of data chains. A FrontierCert light client checks the anchor and parent hashes, the frontier root, the signer bitmap, and the aggregate signature. It opens only the coordinates it needs and never replays the control DAG.

These results belong to the weather-reading and two-plane designs, and the parent-local sources make no slashing claim. Parent-local recovery keeps three portable finality proofs, FAST, FIN, and a certificate for an Ocean resolution, each checked back to genesis. An Ocean certificate must also show that its record came first for its parent.

Every fault counts against one f

Ocean never waits for a fast proposal, for application execution, or for another parent's resolution. Parent-local recovery counts every fault against one budget: at most f identities may deviate, disappear, or lose their safety state. That leaves 4f+1 validators that eventually respond, exactly the size of FAST, a closure set, and an Ocean parent set. The weather-reading design splits the budget, and its 3δ slow path stays live with f Byzantine plus f crashed validators under partial synchrony. The draft calls this 20+20, and its 3f+1 threshold clock makes it possible. It reads Hydrangea's Theorem 3 as ruling out a free 2δ path at 20+20 for f ≥ 3, so that path needs granular synchrony.

One budget, counted two ways. At f = 2 and n = 11, the weather-reading design's 3δ slow path stays live with 2 Byzantine and 2 crashed validators. The 7 honest live validators meet its 3f+1 clock, but cannot guarantee a 4f+1 fast certificate. Parent-local recovery counts every fault against one f, so 9 honest validators eventually respond. That is exactly the size of FAST, a closure set, and an Ocean parent set, with no slack.

Under that split, only 3f+1 honest validators might respond, and a 3f+1 status set can miss every honest signer of a FIN. With f validators silent, FAST needs every remaining one, so River's latency follows the slowest honest response. An offline leader costs one closure, and the cost bound counts closures, not faulty identities. That closure touches one parent, never revokes a certified descendant's signing rights, and its fallback child moves the leader schedule on. Under the stated service assumptions, a stalled parent gets one certified successor almost surely, though that alone promises no transaction rate.

Over a million checks, no violation

A signed reference kernel and an Ocean adapter pass 32 tests, including 28,591 finite quorum-intersection checks and late FAST and FIN assembly. A bounded extension model explored 5,554 worlds and 1,112,888 prefix checks without a violation. The two-plane design's 105 proof gates rebuild from clean on a pinned toolchain, exit 0. They mix all-N invariants in Ivy and mypyvy, SMT checks at f = 1, 2, 3, and Rust harnesses that compare model with kernel. The weather-reading design's confluence proof reduces to one threshold-clock rule: a cone reaches round R only with round-R blocks from 3f+1 distinct authors. Each design's checks cover its own transition system, and their counts do not add up across designs.

In the weather-reading design, 11 nodes across four continents rode out a 360-second storm. River held still, and the second reader kept the log committing at about 0.53 commits per second. The trigger is a pure function of the DAG, so 9 of 11 nodes flipped at one identical round with no coordination. The other 2 had not reached that round, and onset came in 1 of 3 leader-failure runs, so this is a demonstration, not a rate. The two-plane paper reports its own run at about 9.9 commits per second in calm and 1.05 in the storm.

Decoupled consensus, layer by layer

Seams by layer. A green seam has a proof in the version on the right, or holds by construction there. Each proof covers that version's own rules, so the clock proof covers the second version's 3f+1 clock. An amber seam is open, and its step number points to the list below.

Each version of Rohu-Paplet decoupled a different seam. The weather version proved for all N that leaving the fast path needs no ceremony. The second version proved for all N that withheld data cannot stall the control clock. The current design closes one parent at a time, keeps every late FAST, and gives finality with no execution attestation. The next step is one design that holds all of these at once. In the figure, a green seam has a proof or holds by construction, and an amber seam is open, numbered as in the list below.

One substrate and one fault budget. The weather proofs use an uncertified DAG with 3f+1 parents and f Byzantine validators, plus f crashes on the 3δ path. Parent-local recovery runs on a broadcast-accepted DAG with 4f+1 parents and at most f faults in total. Its receipt count does not carry over to the mixed fault model. The plan is to fix the total-f contract, where 2f+1 receipts are tight for one-shot recovery. The two readers then need new definitions on that DAG. The anchor rule R3 goes too, because no cone can hold the votes it asks for.
A weather law for each parent. The weather cycle already has a form for each parent. A local timeout closes one parent's domain, and closing waits for no one. The first valid resolution for that parent is one ordered object, and its certified child opens the next domain. The missing theorem says that River returns to steady 2δ operation once the network is calm. The design already names its premise, a persisted timer floor that must grow past the honest fast-path delay.
A checkpoint child. The Heal did more than end a storm. It bound the executed state root, and it was the activation point for membership changes. Without it, retained history can grow without bound, and the committee stays fixed. The next object is a certified child that binds the semantic identity, frontier, log commitment, application cursor, and configuration. Its proof must show that every closed domain stays closed after compaction.
One native runtime with data on the wire. The goal is one validator that runs DA, cuts, River, closure, resolution, execution, and restart together. Then each seam gets a measurement on hardware, with distinct payloads and a per-position oracle.
Machine-checked parent-local proofs. The one-child, prefix, and independence theorems are hand proofs today, backed by 32 signed tests. The plan is to model closure, protect(S), and the first-resolution rule in the same all-N tier that checked confluence.
A computational coin. Ocean's progress bound uses an ideal coin that stays fresh given the whole prior history. Valid threshold BLS shares alone do not give that. A finite-horizon reduction would bound the chance of no core hit in t waves by (1−Q/n)^t plus the reduction's error.
Fresh data in the first vote. Today a leader must push complete evidence or wait for retrieval, and fresh data needs six message delays. Reaching 2δ for fresh data means a new voting object, with a preservation theorem for prefixes of different lengths.

The full paper, with every proof, equation, and figure, is at /paper.