Pith. sign in

REVIEW 3 major objections 5 minor 6 references

Frosty for partial synchrony

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Appending the Frosty liveness module to Snowman⋄ preserves consistency and liveness in partial synchrony, for f < n/5 and n ≥ 250.

desk verdict A useful combination note with a real gap: the cross-epoch consistency proof imports (⋄1) without showing the new alpha3 finality rule preserves it. read the letter →

arxiv 2506.09823 v1 pith:OOUWK46C submitted 2025-06-11 cs.DC

Stephen Buttolph , Andrew Lewis-Pye , Kevin Sekniqi This is my paper · ORCID
classification cs.DC
keywords FrostySnowman⋄partialsynchronylivenessmoduleconsensusepochchangeSimplexstartingcertificate
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This note shows that the Frosty liveness module, previously designed for the synchronous Snowman protocol, can be adapted to run on top of the partially synchronous Snowman⋄ protocol. The authors give two algorithms that split execution into even epochs running Snowman⋄ and odd epochs running a Simplex-based quorum protocol, connected by starting certificates. They argue that, for n ≥ 250 and f < n/5, the protocol preserves consistency across epochs and ensures liveness with small error probability, measured under bounded executions. The result matters because it gives Snowman-style consensus the liveness guarantees of Frosty without requiring a synchrony assumption.

What carries the argument

The central machinery is the epoch structure with starting and epoch certificates. A starting certificate is a set of at least 4n/5 signed starting votes, and Pref(C) is the longest chain extended by more than half of those votes; this bridge forces values finalized in an odd epoch to extend all even-epoch final values. An epoch certificate is a set of at least n/5 stuck messages that triggers movement into the next odd epoch. The other load-bearing piece is the new finality condition (α3 = 48): two consecutive samples in which at least 3/5 of the sampled processes report final values extending σ allow a process to finalize σ, which keeps epoch changes timely. In odd epochs, Simplex with notarizations and finalizations ensures quorum-based consistency.

What would settle it

Run the even-epoch protocol with n = 250, f = 50, k = 80, α3 = 48 under an adversarial scheduler that controls sample sequences, and check whether a correct process can finalize a value σ via the α3 rule while fewer than 3/4 of the correct processes later include σ in their starting votes; exhibiting such an execution would invalidate (⋄1) and break the cross-epoch consistency argument.

Watch

Extended reading notes

Core claim

The central claim is that Algorithms 1 and 2 define a Frosty extension of Snowman⋄ that is consistent and live in the standard partial synchrony model: consistency holds at all times, and after GST liveness holds except for small error probabilities. Consistency across an even-to-odd epoch boundary is carried by the starting certificate: since each starting vote extends the previous even-epoch final value when event (⋄1) holds, Pref(C) extends every value finalized in the previous even epoch. Within even epochs the new α3 finality rule is shown safe because, conditioned on event (⋄0), it only finalizes a value already finalized by a correct process. Liveness is established by showing that, within bounded time after GST, either all correct processes advance their final value or all enter the odd epoch, where Simplex finalizes a new value.

Load-bearing premise

The cross-epoch consistency proof relies on event (⋄1): that whenever a correct process finalizes a value in an even epoch, more than 3/4 of correct processes that later send a starting vote extend that value, and this event is imported from the proof for the unmodified Snowman⋄ protocol without a proof that the new α3 finality rule preserves it.

Editorial extensions

If this is right

  • Frosty can be used with Snowman⋄ in partial synchrony, so the communication-complexity advantages of Snowman during normal operation are preserved while liveness attacks by adversaries up to f < n/5 are handled.
  • Consistency between even and odd epochs is guaranteed with error probability at most about 2×10⁻⁵ plus the small probability of (⋄0) failing, under the stated execution bounds.
  • An odd epoch finalizes at least μ Simplex blocks and then returns to Snowman⋄; the choice of μ and γ are parameters to be set by the implementer.
  • Epoch changes can now be triggered by long periods of asynchrony as well as deliberate liveness attacks, so γ should be chosen large enough to avoid spurious epoch changes.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper imports event (⋄1) from the Snowman⋄ consistency proof, but that proof was for the unmodified even-epoch protocol; because the new α3 finality rule changes even-epoch behavior, the cross-epoch consistency argument has a missing load-bearing link unless (⋄1) is re-established under the modification.
  • A natural testable extension is to verify (⋄1) computationally for the modified protocol around f = n/5, checking whether more than 3/4 of correct starting votes extend a value finalized under the α3 rule in worst-case sample sequences.
  • The parameter values (n ≥ 250, f < n/5, k = 80, α3 = 48) are chosen to make binomial estimates simple; the same structure likely works for other parameter ranges but with different error bounds.
  • The authors note that periods of asynchrony alone can trigger an epoch change, so in deployments γ must be calibrated against realistic asynchrony durations; this is a tuning concern the paper leaves to practice.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper specifies Frosty, a liveness module, on top of Snowman⋄ for the partially synchronous setting. It proposes a two-epoch structure: even epochs run Snowman⋄ with an added decision condition (α3) that lets a process finalize a value when two consecutive samples contain at least α3 reports of finalized values extending it, while odd epochs run Simplex, initialized from a starting certificate of 4n/5 starting votes. The main claim is that for k=80, α1=41, α2=72, α3=48, β=14, γ≥300, n≥250, and f<n/5, the protocol maintains consistency across even and odd epochs and ensures liveness with small error probability under bounded executions. The consistency proof imports the lemma (⋄1) from [3] and separately proves a local lemma (⋄0) for the new α3 rule; the liveness proof assumes that the set E of available child blocks is never empty.

Significance. If correct, the contribution is practically relevant: it would extend the Frosty liveness module from the synchronous Snowman+ setting to the partially synchronous Snowman⋄, with explicit parameters and concrete error bounds, and it identifies Simplex as the fallback protocol. The paper is transparent about inherited assumptions and provides protocol pseudocode at a level suitable for subsequent implementation. However, the central cross-epoch consistency theorem is not established as written because the key lemma (⋄1) is imported from a protocol without the new α3 finalization rule, and no proof is given that the new rule preserves the lemma. The liveness result is also conditional on an unproved assumption about block availability. These gaps are local and likely repairable, but they are load-bearing for the stated claims.

major comments (3)
  1. [Section 6.1, event (⋄1)] The proof that Pref(C) extends every even-epoch final value relies on (⋄1), which is imported from [3] for 'any correct process finalizes σ while in an even epoch'. The protocol analyzed in [3] does not include the new finality condition given in Algorithm 2, line 52. That new condition creates additional finalization events, and the present paper proves only (⋄0) for those events. (⋄0) says that some correct process has already finalized a value extending σ; it does not say that more than 3/4 of the correct processes that later send starting votes extend σ, nor does it control starting votes sent before the α3-based finalization. Obtaining (⋄1) for an α3-finalized σ would require an induction over finalization events, showing that the earlier finalization τ⊇σ itself has the required starting-vote property, and if τ is also α3-finalized the argument must recurse. No such inductive proof is supplied. Without (⋄1), a starting certificate may fail to extend an even-epoch final value, so the cross-epoch consistency claim is not proved.
  2. [Section 6.2, first paragraph] Liveness is proved under the assumption that the set E specified in Algorithm 2, line 26 is never empty for correct processes when they begin the while loop. This is a substantive liveness assumption that is not derived from the partial-synchrony model or from any block-proposal mechanism. The abstract and Section 1 state the result without this qualification. The theorem should be stated with this caveat, or the assumption should be justified by an explicit argument that new blocks are always available to correct processes.
  3. [Section 6.1, final paragraph] The text says 'From (⋄1) and the fact that f>n/5 it follows that σ⊆Pref(C)'. The inequality should be f<n/5; with f>n/5 the implication is reversed. This step is the bridge from (⋄1) to cross-epoch consistency, so the inequality must be corrected and the arithmetic checked.
minor comments (5)
  1. [Section 3 vs Section 6] Section 3 states β=12, while Section 6 uses β=14 for the analysis; the discrepancy should be reconciled.
  2. [Algorithm 2, line 52] Condition (ii) reuses s′ as both the starting round of the interval and the index in rfin(j,s′,e); it should read rfin(j,s″,e) inside the quantification over s″.
  3. [Section 6.1, probability bound for (⋄0)] The bound 2×10^{-13} is computed under the stated cap of 10,000 processes, 1000 years, and 5 rounds per second; this finite execution bound should be made part of the theorem statement, since the error probability grows with execution length.
  4. [Footnote 4] The footnote raises the partial-hash issue for the final block in Pref(C) but only says it 'requires consideration'; a sentence explaining why the partial hash does not affect consistency or liveness would remove ambiguity.
  5. [Section 6.1, derivation of (⋄0)] The proof of (⋄0) is only sketched by reference to [2]; since [2] analyzes a different Snowman variant in the synchronous setting, a self-contained derivation of the binomial bound would strengthen the paper.

Circularity Check

1 steps flagged · score 4.0 of 10

Cross-epoch consistency rests on (⋄1) imported from the authors' own [3], which did not include the new alpha3 finality rule; the missing inductive transfer from (⋄0) to (⋄1) is the load-bearing self-citation.

  1. self citation load bearing [Section 6.1, 'The proof of consistency' (cross-epoch consistency argument)]
    "The proof of Section 8 of [3] establishes that (⋄1) below holds for the entirety of an execution, except with probability at most 2×10−5: (⋄1): Whenever any correct process p_i finalizes some σ while in an even epoch e, the following is true of more than 3/4 of the correct processes p_j: if p_j ever sends a starting vote (start,e+1,σ′), then σ⊆σ′."

    Cross-epoch consistency reduces to (⋄1): the paper immediately uses it to conclude σ⊆Pref(C) and hence σ⊆σ′. The citation is the authors' own [3], whose Section 8 proof concerns Snowman⋄'s original finality rule, not the new alpha3 decision condition introduced here in Algorithm 2, line 52. The paper proves only (⋄0) for alpha3 finalizations—that a correct process already finalized an extending value—and does not prove that the imported 'more than 3/4 of correct processes' property transfers to alpha3-finalized values, nor give the needed induction from (⋄0) to (⋄1). Thus the central consistency claim depends on an unverified self-citation whose stated assumptions omit the modified protocol. This is load-bearing self-citation rather than a fitted-parameter reduction.

full rationale

The paper contains no fitted parameters and no prediction that is a renamed fit; the protocol parameters are fixed analysis assumptions, and liveness/consistency claims are direct probabilistic calculations. The one load-bearing external input is (⋄1), imported from the authors' preprint [3]. Because [3] analyzes Snowman⋄ without the alpha3 finality rule added here, (⋄1) is not established for the modified even-epoch protocol, and the paper gives only (⋄0) rather than the required inductive transfer to (⋄1). This makes the cross-epoch consistency proof rely on a self-citation rather than on a derivation contained in the note. That is a circularity burden (score 4), not a full reduction-by-construction (score 6+), since the alpha3 safety calculation, liveness proof, and Simplex integration are independently presented and the gap appears repairable.

Assumptions & free parameters 9 free parameters · 6 assumptions · 0 invented entities

The protocol introduces no new physical or cryptographic entities; it recombines existing algorithmic objects (epoch certificates, starting certificates, dummy blocks) from [2] and [4]. The unpaid intellectual debts are the inherited (diamond1) lemma and Simplex properties, plus the E-nonempty liveness assumption. The many hand-set parameters (k, alpha1, alpha2, alpha3, beta, gamma, mu, thresholds) are protocol constants tuned to make the probabilistic proof work, not derived from a uniqueness theorem.

free parameters (9)
  • k (sample size) = 80
    Sample size for Snowman diamond polls; chosen so that binomial probability calculations for alpha thresholds are clean.
  • alpha1 (preference threshold) = 41
    Threshold used in Algorithm 2 lines 33-35 to update pref; chosen for proof convenience.
  • alpha2 (lock threshold) = 72
    Threshold for locks and support in Algorithm 2 lines 15, 19-22, 39-42; chosen for proof convenience.
  • alpha3 (new finality condition threshold) = 48
    Extra finality threshold in line 52; set to 3/5 of k so the probability of at least 48 Byzantine sample positions is less than 1e-14.
  • beta (consecutive rounds for finalization) = 14
    Parameter in line 51 for Snowman diamond finalization; chosen for proof convenience.
  • gamma (stuck rounds before epoch certificate) = at least 300
    Line 56; chosen to make liveness failure probability less than 1e-18 and to reduce spurious epoch changes under asynchrony.
  • mu (reduced height to finish odd epoch) = chosen to taste (positive integer)
    Determines how many Simplex blocks finalize an odd epoch before returning to Snowman diamond; no specific value given.
  • epoch-certificate threshold = n/5
    Number of (stuck,e,sigma) messages forming an EC; set to match the adversary bound f less than n/5 so the adversary alone cannot force epoch changes.
  • starting-certificate threshold = 4n/5
    Number of starting votes required for an SC; combined with more than 3/4 correct-process extension in (diamond1) to ensure Pref(C) extends all final values.
assumptions (6)
  • domain assumption Authenticated point-to-point channels, PKI, collision-resistant hash, and perfect cryptography (adversary cannot forge signatures or break hashes).
    Standard cryptographic model stated in Section 2; used for uniqueness of hash values and validity of signed messages.
  • domain assumption Static Byzantine adversary controls up to f processes with f less than n/5, and n at least 250.
    Section 2 and Section 6; the adversary bound is inherited from [3] and drives all binomial probability calculations.
  • domain assumption Partial synchrony: known Delta, unknown GST; messages sent at time t arrive by max(t,GST)+Delta; correct clocks proceed in real time.
    Section 2; the liveness argument uses the post-GST Delta-bounded delivery to time epoch changes.
  • domain assumption Lemma (diamond1) from [3]: if a correct process finalizes sigma in even epoch e, then more than 3/4 of correct processes that later send starting votes for e+1 extend sigma, except with probability at most 2e-5.
    Invoked in Section 6.1 to prove Pref(C) extends sigma; not reproved and not verified against the new alpha3 finality rule.
  • domain assumption Simplex quorum intersection and liveness from [4] continue to hold for the modified Simplex with dummy blocks and starting certificates.
    Section 6.1 (Consistency within odd epochs follows as in [4]) and Claim 4.
  • ad hoc to paper For the liveness proof, the set E of child blocks available to extend pref is never empty for correct processes.
    Section 6.2 explicitly assumes new blocks always exist; the general transaction-arrival case is not analyzed.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Frosty for partial synchrony." pith.science (2026). https://pith.science/paper/OOUWK46C

@misc{pith2026250609823,
  author       = {Pith},
  title        = {Pith review of: Frosty for partial synchrony},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OOUWK46C}},
  note         = {Machine review of arXiv:2506.09823}
}
read the original abstract

Snowman is the consensus protocol used by blockchains on Avalanche. Recent work has shown both how to augment Snowman with a `liveness' module called `Frosty' that protects against liveness attacks, and also how to modify Snowman so as to be consistent in partial synchrony. Since Frosty assumes (a strong form of) synchrony, the aim of this note is to show how to modify Frosty to deal with the partially synchronous version of Snowman.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

6 extracted references · 5 canonical work pages

  1. [2]

    Frosty: Bringing strong liveness guarantees to the snow family of consensus protocols.arXiv preprint arXiv:2404.14250, 2024

    Aaron Buchwald, Stephen Buttolph, Andrew Lewis-Pye, Patrick O’Grady, and Kevin Sekniqi. Frosty: Bringing strong liveness guarantees to the snow family of consensus protocols.arXiv preprint arXiv:2404.14250, 2024

    arXiv 2024

  2. [3]

    Snowman for partial synchrony

    Aaron Buchwald, Stephen Buttolph, Andrew Lewis-Pye, and Kevin Sekniqi. Snowman for partial synchrony.arXiv preprint arXiv:2501.15904, 2025

    work page Pith review arXiv 2025

  3. [1]

    Short signatures from the weil pairing

    Dan Boneh, Ben Lynn, and Hovav Shacham. Short signatures from the weil pairing. InInternational conference on the theory and application of cryptology and information security, pages 514–532. Springer, 2001

    work page 2001

  4. [4]

    Simplex consensus: A simple and fast consensus protocol

    Benjamin Y Chan and Rafael Pass. Simplex consensus: A simple and fast consensus protocol. InTheory of Cryptography Conference, pages 452–479. Springer, 2023

    work page 2023

  5. [5]

    Jolteon and ditto: Network-adaptive efficient consensus with asynchronous fallback

    Rati Gelashvili, Lefteris Kokoris-Kogias, Alberto Sonnino, Alexander Spiegelman, and Zhuolun Xiang. Jolteon and ditto: Network-adaptive efficient consensus with asynchronous fallback. InInternational conference on financial cryptography and data security, pages 296–315. Springer, 2022. Stephen Buttolph, Andrew Lewis-Pye, and Kevin Sekniqi11

    work page 2022

  6. [6]

    Practical threshold signatures

    Victor Shoup. Practical threshold signatures. InAdvances in Cryptology—EUROCRYPT 2000: International Conference on the Theory and Application of Cryptographic Techniques Bruges, Belgium, May 14–18, 2000 Proceedings 19, pages 207–220. Springer, 2000

    work page 2000

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.