{"id":"0375c5a0-a503-4823-b534-d4df127d16a2","arxiv_id":"2608.13434","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A modified Tendermint protocol that decides in two communication steps under n > 5f, with safety and liveness proofs and a Quint model-checked specification.","lead":"Fast Tendermint adapts the widely used Tendermint consensus protocol to tolerate fewer Byzantine faults (n > 5f) in exchange for deciding in two communication steps instead of three. If correct, this could lower blockchain transaction latency while keeping Tendermint's simple round-based leader rotation.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The termination proof has a gap: Lemma 6 assumes all correct processes enter round r within Δ of the first, but the quorum-any round advance (line 34/46) provides no catch-up bound for processes behind at GST.","rationale":"I read the paper as a focused protocol adaptation whose central claim is that Fast Tendermint preserves Tendermint's structure while achieving Agreement, Validity, and Termination with two-step good-case latency. The safety argument is plausible: Lemma 2's induction is informal but points to the right intersection argument, Theorem 3's Agreement proof follows if Lemma 2 holds, and Validity is handled by tracing the earliest correct precommit to the fresh-proposal rule. The decision rule's loose round binding (fresh proposal round r and precommit round r′) is unusual but does not break Agreement, since the minimum precommit round still controls the Lemma 2 argument.\n\nThe load-bearing weakness is liveness, specifically the transition from 'first correct process enters round r' to 'every correct process enters round r by t+Δ' in Lemma 6. The reader's weakest assumption identified Theorem 7's asserted existence of a good round and the unspecified adaptive timeout schedule. I partially agree, but I would sharpen the concern: even if timeouts are chosen large enough and a correct proposer eventually appears, Lemma 6 applies only if all correct processes are close enough in round number to vote in the same round. The protocol's round-skip mechanism is timeout-based, not an immediate jump, so a process behind at GST may remain behind indefinitely; Theorem 7 never proves convergence of all correct processes to a common round within bounded skew.\n\nI do not move the verdict to REJECT because no concrete counterexample is established and the gap may be repairable by adding a catching-up lemma or by changing the round-skip rule. I also give credit for the Quint specification being made available, although the paper does not report which properties or instances were model-checked. The verdict should remain CONDITIONAL, with the condition being a rigorous liveness proof or a successful liveness model-check under skewed initial rounds.","tokens_in":7955,"tokens_out":37658,"duration_ms":398888,"concrete_test":"Use the authors' Quint specification to model-check a termination liveness property for n=6, f=1, with an initial post-GST configuration in which correct processes are split across three different rounds and the first two proposers are Byzantine. Ask TLC/Quint whether there is a reachable execution in which no round ever accumulates n−f matching precommits. If a liveness violation or an infinite-timeout trace is found, Theorem 7 is refuted for that instance; if the property verifies, the current proof gap may be repairable and the CONDITIONAL verdict stands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The weakest load-bearing point is in Lemma 6 and Theorem 7. Lemma 6 assumes that if the first correct process enters round r at time t, then every correct process enters round r by t+Δ. This does not follow from the gossip property unless every correct process is already in round r−1 and has scheduled timeoutPrecommit(r−1) after receiving the same n−f quorum. The protocol's only round-advance path is line 34, which schedules a timeout for some future round r′ upon receiving n−f precommits for that round, followed by OnTimeoutPrecommit starting round r′+1 (lines 46-47). A correct process that is several rounds behind at GST can therefore receive n−f precommits from a future round, wait timeoutPrecommit(r′), and start at r′+1 only after the first correct process has already moved on. There is no immediate f+1-style jump, and Theorem 7's assertion that adaptive timeouts 'increase over rounds' does not by itself prove that a permanent round lag is closed. If any correct processes are behind, fewer than n−f correct processes may be able to precommit in the deciding round, so the decision rule never fires. Thus termination is asserted rather than established, and the correctness of the central claim is conditional on a missing liveness lemma.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents Fast Tendermint, a modification of the Tendermint BFT consensus protocol for systems with n > 5f Byzantine processes. The main idea is to collapse Tendermint's prevote and precommit steps into a single PRECOMMIT step and to merge the locked and valid state variables, which yields two communication steps in the good case (propose, then precommit). The paper claims Agreement, Validity, and Termination in the partially synchronous model with a gossip communication property, and it accompanies these claims with hand-written proofs and a Quint/TLA+ specification used for model checking.","tokens_in":8204,"tokens_out":35340,"duration_ms":345042,"significance":"If the result is correct, the paper makes a useful contribution: it shows that a relatively small modification of a widely deployed consensus protocol can achieve two-step good-case latency under the n > 5f fault-tolerance assumption, while retaining Tendermint's round-rotation mechanism. The safety proofs are careful and the counting arguments are consistent with the n > 5f threshold. The paper also provides a formal specification in Quint, which is a concrete asset. However, the termination proof is currently a sketch rather than a rigorous derivation, and the adaptive timeout schedule on which liveness depends is not specified. Since Termination is one of the three central claimed properties, this gap is load-bearing and must be addressed before the paper can be accepted.","major_comments":[{"comment":"Termination is asserted rather than proved. Theorem 7 states that after GST there is guaranteed to be a round r satisfying Lemma 6, with a correct proposer and with t > GST + timeoutPrecommit(r−1), timeoutPropose(r) > 2Δ + timeoutPrecommit(r), and timeoutPrecommit(r) > 2Δ, but no argument is given that the protocol's round progression actually reaches such a round. The adaptive timeout schedule is never defined, and the statement that timeouts \"increase over rounds\" does not by itself show that a round satisfying all of Lemma 6's conditions eventually occurs. In particular, condition (1) requires the round to start after GST plus the previous round's precommit timeout, and the proof must show that the waiting time for round r eventually exceeds this bound. Because Termination is one of the three stated properties, this gap is load-bearing for the paper's main claim.","section":"§4, Theorem 7"},{"comment":"Lemma 6's proof assumes without derivation that every correct process enters round r within Δ of the first correct process. This conclusion is not automatic: the first correct process enters r because its timeoutPrecommit(r−1) expired after it received an n−f precommit quorum for round r−1, but that quorum may contain Byzantine-signed messages that were received by only a subset of correct processes. The proof must explicitly use the second clause of the gossip property, which propagates any message received by a correct process, to show that every correct process receives the same quorum and therefore schedules the same timeout and enters round r by t+Δ. Lemma 5's proof has the same unstated propagation step when it infers that all correct processes schedule the timeout at most Δ after proposer p. These steps are likely fixable, but as written they are a gap in the derivation of Lemma 6 and hence in the liveness argument.","section":"§4, Lemma 6"}],"minor_comments":[{"comment":"The decision rule pairs a fresh proposal for round r with n−f precommits for a value from an arbitrary round r′, without stating the relationship between r and r′. The proof of Theorem 3 refers to \"the round rp\" of the precommits, so the pseudocode should say explicitly that safety holds for any r′ and that the proposal round is not used in the agreement argument.","section":"Algorithm 1, line 36"},{"comment":"The functions timeoutPropose(r) and timeoutPrecommit(r) are never defined. A concrete adaptive schedule is needed for the termination proof to be verifiable; for example, the paper could specify a deterministic increasing function of the round number and prove that the timing conditions of Lemma 6 are eventually satisfied.","section":"§2 and §4"},{"comment":"The claim that the protocol was model-checked in Quint would be more informative if the paper reported the parameters checked, such as the values of n and f, the number of rounds explored, and the properties verified.","section":"§1 and §4"},{"comment":"The phrasing \"Any two sets of n−f and 2f+1 processes\" should be \"Any two sets of size n−f and 2f+1 processes\" for clarity.","section":"§4, Lemma 1"},{"comment":"In the sentence \"Since p scheduled it after GST\", the pronoun \"it\" is ambiguous; it should read \"Since p scheduled timeoutPrecommit(r−1) after GST\".","section":"§4, Lemma 5"},{"comment":"The phrase \"all n−f correct precommits\" is imprecise; there are n−f correct processes in the good case, and the proof should say that the n−f precommits broadcast by those processes are received by all correct processes within 2Δ, using the gossip property applied to each send.","section":"§4, Lemma 6"}],"recommendation":"major_revision","confidential_remarks":"The safety part of the paper is careful and appears sound, but the liveness proof is the main weakness. The authors should be asked to provide a rigorous termination proof with an explicit timeout schedule and a lemma showing that all correct processes eventually enter the same round after GST. If this cannot be done, the paper's central claim of Termination would not be supported. The paper is otherwise a good fit for the journal."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know two things about this paper. First, the core contribution is real: it takes Tendermint, drops the prevote step, merges locked and valid, and gets two-step good-case finality under n>5f while keeping the per-round leader rotation. Second, the safety side is in decent shape, but the liveness proof is not. The termination theorem is asserted, not derived.\n\nWhat the paper does well: the adaptation is minimal and clearly presented. The counting arguments in Lemma 2 and Theorem 3 are careful and consistent with the n>5f threshold. The validity proof is clean. The authors also situate the work honestly in the literature, crediting FaB Paxos, Minimmit, BlueBottle, and the 5f-1 tight bound. They ship a Quint specification, which is a real artifact.\n\nThe soft spots are proportionate. The load-bearing one is the termination gap. Lemma 6 assumes all correct processes enter round r within Delta of the first correct process. That does not follow from the gossip property given the protocol's only round-advance path: the quorum-any rule schedules a timeout for a future round, and a process that is several rounds behind at GST can stay behind forever if adaptive timeouts keep growing. Theorem 7's claim that eventually a round satisfies the lemma's conditions is exactly the missing lemma. This is not a minor stylistic issue; without it termination is unproven. Second, the decision rule in line 36 uses r' without binding it to the proposal round r. The prose says \"matching\" precommits, but the pseudocode should be explicit that r'=r. That is minor but confusing. Third, the Quint model-checking claim is vague: no details on instance sizes, what properties were checked, or how far the check went. Since model checking cannot establish unbounded termination, this doesn't fix the gap.\n\nThe reader's conditional verdict is fair, and the stress-test note correctly identifies the weakest point. This paper is for the BFT consensus community, particularly people working on low-latency blockchains who want a minimal modification of a deployed protocol. It deserves a serious referee, but the termination proof needs a real liveness lemma, and the pseudocode needs cleaning up before it is acceptable.","headline":"A clean and honest two-step Tendermint variant for n>5f with plausible safety proofs, but the termination argument has a real gap and the model-checking claim is underspecified.","tokens_in":8746,"tokens_out":1936,"would_cite":false,"duration_ms":21545,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68M14","68M15","68M20"],"pacs":[],"model":"deepseek-v4-flash","headline":"A two-step variant of Tendermint for networks with fewer faults","keywords":["BFT consensus","Tendermint","partial synchrony","good-case latency","Byzantine faults","leader rotation","Quint specification","consensus protocol"],"falsifier":"A concrete counterexample would be a schedule of adaptive timeouts and a round sequence in which, after GST, every round with a correct proposer has one of the timing conditions of Lemma 6 violated (e.g., timeoutPropose(r) not exceeding 2∆ + timeoutPrecommit(r) or timeoutPrecommit(r) not exceeding 2∆), so that no round ever yields a decision, showing termination fails.","tokens_in":7746,"feed_emoji":"⚡","tokens_out":1427,"duration_ms":15990,"temperature":0.7,"pith_summary":"The paper claims that a lightly modified Tendermint consensus protocol can decide in two communication steps, not three, by assuming a stricter fault budget of $n > 5f$ instead of the usual $n > 3f$. The key move is to drop the prevote round entirely and let a single round of precommits, together with the proposal, determine the decision. A sympathetic reader would care because Tendermint is already widely deployed in blockchains, and a shorter good-case latency translates directly to faster finality without abandoning Tendermint's simple, per-round leader rotation.","feed_headline":"Tendermint variant decides in two steps when faults are capped at 20%","feed_subtitle":"Fast Tendermint drops the prevote round and merges state to cut good-case latency from three communication steps to two.","key_machinery":"The central object is the merged valid state $(round, value)$ that a process updates only after observing $2f+1$ precommits for a value in a round, plus the observation rule and re-proposal rule that carry safety across rounds. This machinery replaces Tendermint's separate locked and valid variables and its two-step voting pipeline, making a single precommit step sufficient to decide when the proposer is correct and the network is synchronous.","core_discovery":"The paper introduces Fast Tendermint, which preserves Tendermint's leader-rotation structure while merging the locked and valid state variables into a single valid pair, and collapsing the prevote and precommit steps into one voting step. In the good case, a correct proposer broadcasts a proposal and processes decide once they have the proposal and $n-f$ matching precommits for a value. The paper proves Agreement, Validity, and Termination in the partially synchronous model with the gossip property, relying on the observation that any $n-f$ quorum and any $2f+1$ quorum of precommits must intersect in a correct process when $n > 5f$.","pith_inferences":["A natural next step is to determine whether a fast path with $n > 5f$ can be combined with a failure-optimal slow path that still tolerates $f < n/3$, an open question the paper itself notes; the current protocol gives up the larger fault budget on the slow path.","The proof of termination rests on an assumption about adaptive timeouts and round rotation after GST, so a concrete implementation would need to specify timeout growth to make the termination guarantee unconditional.","The two-step good-case latency of Fast Tendermint could plausibly be measured against Tendermint's current latency in a testbed, providing an experimental check on how much of the theoretical speedup survives in real network conditions.","The paper's decision rule, which triggers on the proposal plus $n-f$ precommits regardless of the receiver's current round, is a distinctive mechanism worth comparing with the decision rules of other $n > 5f$ protocols to see whether it yields a simpler liveness proof."],"forward_implications":["Fast Tendermint shows that an existing, production-grade consensus protocol can be adapted to the $n > 5f$ setting without introducing complex view-change machinery, potentially lowering the barrier to adopting faster finality in blockchains.","If correct, the protocol inherits the two-step good-case latency of other $n > 5f$ protocols while maintaining Tendermint's simple round-based leader rotation, which could make it easier to deploy in existing Tendermint-based systems.","The proof that a single precommit round suffices relies on the quorum intersection $n-f$ and $2f+1$ overlapping in a correct process, a property that holds exactly when $n > 5f$, so the protocol does not extend to the tighter $n \\geq 5f-1$ bound without additional mechanisms.","The paper's formal specification in Quint, model-checked, provides a machine-checkable artifact that can be reused for future modifications to the protocol.","The protocol's slow path remains simple but nontrivial: when the proposer is faulty or the network is asynchronous, processes fall back to multi-round operation controlled by adaptive timeouts, preserving termination at the cost of latency."],"supporting_citations":[{"why":"Defines the original Tendermint consensus algorithm and its system model, which Fast Tendermint adapts.","marker":"[5]"},{"why":"Introduces the partially synchronous model with GST that the paper uses for all correctness proofs.","marker":"[11]"},{"why":"Provides the lower bound on good-case latency that motivates the claim that three communication steps are necessary when $f < n/3$.","marker":"[1]"},{"why":"Shows that two-step consensus is achievable at the tighter bound $n \\geq 5f-1$, framing the paper's choice of $n > 5f$.","marker":"[15]"},{"why":"Supplies the Quint specification language used to model-check the formal protocol description.","marker":"[12]"},{"why":"Presents a related $n > 5f$ protocol, Minimmit, with a view-progression rule similar to Fast Tendermint's observation rule, used as a comparison point.","marker":"[9]"},{"why":"Presents BlueBottle, another $n > 5f$ two-step protocol, as a related DAG-based approach against which Fast Tendermint is compared.","marker":"[26]"}],"fun_headline_variants":["Fast Tendermint: two-step consensus with 20% fault cap","Tendermint's two-step upgrade: good-case latency halved","Speeding Tendermint: decide in two steps when f < n/5","Fast Tendermint: same rotation, half the communication steps"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The termination proof assumes that after the network stabilizes, a round eventually starts with a correct proposer while the adaptive timeout values satisfy the timing inequalities of Lemma 6, but the paper asserts this without proving that such a round exists.","fun_headline_variants_meta":{"raw":{"variants":["Fast Tendermint: two-step consensus with 20% fault cap","Tendermint's two-step upgrade: good-case latency halved","Speeding Tendermint: decide in two steps when f < n/5","Fast Tendermint: same rotation, half the communication steps"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000752,"raw_usage":{"total_tokens":3310,"prompt_tokens":874,"completion_tokens":2436,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":490,"completion_tokens_details":{"reasoning_tokens":2357}},"tokens_in":490,"tokens_out":2436,"duration_ms":16606,"temperature":1.0,"reasoning_tokens":2357,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:07:40.794887+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A concrete counterexample would be a schedule of adaptive timeouts and a round sequence in which, after GST, every round with a correct proposer has one of the timing conditions of Lemma 6 violated (e.g., timeoutPropose(r) not exceeding 2∆ + timeoutPrecommit(r) or timeoutPrecommit(r) not exceeding 2∆), so that no round ever yields a decision, showing termination fails.","supporting_citations":[{"cited_title":"8 Fast Tendermint 13 Informal Systems and Circle Internet Financial","cited_arxiv_id":null,"evidence_quote":"Defines the original Tendermint consensus algorithm and its system model, which Fast Tendermint adapts."}],"review_version":1}