{"id":"23cf159c-7358-41a1-ab3f-70b4a0bea6ce","arxiv_id":"2504.16853","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"full","parameter_count":0,"one_line_summary":"A machine-checked ACL2 proof shows that a DAG-based BFT consensus protocol with dynamic stake never forks, provided faulty stake in every committee is below one third.","lead":"This paper uses the ACL2 theorem prover to prove that a DAG-based blockchain consensus protocol with validator stake that can change at every block never forks. The proof is machine-checked and covers arbitrarily long executions, but it assumes that faulty stake in every active validator set stays below one third.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the ACL2 machine-checked invariant proof appears internally sound, and the acknowledged model-adequacy trust boundary is a standard, clearly stated limitation rather than a fixable flaw.","rationale":"The reader correctly identifies model adequateness as the load-bearing premise. That is the only route by which the theorem could fail to say something about a real DAG-based BFT protocol. My review did not find a concrete internal gap in the ACL2 model or in the proof structure. The transition rules are conservative in the right places: acceptance re-checks signer quorum, the bcmt bottom guard prevents stale validators from calculating committees they should not yet know, and the interdependent invariants are proved by simultaneous induction rather than by a hidden circular argument. The paper also clearly states the trust boundary, so the central claim, which is about the formal model, is exactly what is proved. The duplicate-certificate abstraction is worth a footnote, because real signatures over a proposal can appear in multiple certificates with the same block and different endorser lists, whereas the model treats endorser membership as tied to one certificate. However, such duplicates carry the same author, round, transactions, and previous references, so they produce the same blocks and do not threaten nonforking. Thus no verdict adjustment is needed.","tokens_in":38227,"tokens_out":30060,"duration_ms":318565,"concrete_test":"Pin the exact commit of the ACL2 book at https://github.com/acl2/acl2/tree/master/books/projects/aleo/bft (recording the submission-time hash), run the full certification in a clean ACL2 build, and inspect the definition of all-system-committees-fault-tolerant-p to confirm it checks the fault-tolerance predicate on every state of the event sequence, including the final state. If the proof certifies and that predicate matches the paper's fault-tolerant-reachable set, the central claim is settled as stated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is about the formal model, so the only meaningful risk is whether the transition relation faithfully over-approximates the protocol's safety-relevant behavior. I checked the usual trouble spots. (1) Certificates created by faulty authors skip the signer-quorum check at creation, but acceptance independently re-checks signer quorum, and the creation rule requires correct endorsers to pass the newness, closure, and previous-quorum checks; equivocal certificates therefore cannot enter a correct validator's DAG. (2) Selective delivery is covered because messages may remain undelivered forever; broadcast-to-all combined with non-acceptance models any subset delivery. (3) A lagging validator cannot calculate active committees for rounds beyond its blockchain's last block plus two, because bcmt returns bottom; this prevents committee disagreement caused by stale blockchains. (4) The apparent circularity between DAG nonequivocation and committee agreement is explicitly resolved by a simultaneous induction. The most delicate abstraction is the atomic multi-step endorsement process, which excludes real executions containing duplicate certificates that differ only in their endorser lists while carrying identical proposal content. Those duplicates are semantically equivalent for blockchain generation, so this does not appear to risk under-approximating a fork, but the paper does not argue this point explicitly.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a formal model of a DAG-based Byzantine fault-tolerant consensus protocol with dynamic stake, inspired by Narwhal/Bullshark and AleoBFT, as a labeled state transition system with four event types. The authors prove, in the ACL2 theorem prover, that the blockchains of any two correct validators are prefix-comparable (blockchain nonforking) in all fault-tolerant-reachable states, where every active committee that validators can calculate has no more than one-third of its stake controlled by faulty validators. The proof proceeds through a series of invariants, including DAG nonequivocation, anchor nonforking, and committee agreement, which are interdependent due to the circular dependency between DAG and blockchain construction; the circularity is resolved by simultaneous induction. The ACL2 formalization is open source, and the paper explicitly states that the transition system is trusted to capture the protocol and that the ACL2 definition of nonforking is trusted to express the intended property.","tokens_in":38408,"tokens_out":8272,"duration_ms":81032,"significance":"This is, to my knowledge, the first machine-checked proof of blockchain nonforking for a DAG-based BFT consensus protocol with dynamic stake, applying to arbitrarily long executions and arbitrarily large system states. The work's main strengths are: (i) the central theorem is machine-checked by ACL2, with the full development available open source; (ii) the proof is not circular in a problematic sense—the interdependence of DAG nonequivocation, committee agreement, and nonforking is handled by a valid simultaneous induction; (iii) the fault-tolerance condition is expressed cleanly in terms of stake, clarifying how the classic less-than-one-third bound generalizes to dynamic committees; and (iv) the paper is unusually explicit about its trust boundary (model adequacy and the ACL2 formulation of nonforking). If the model is accepted as a faithful abstraction, the result is a solid and valuable contribution to the formal verification of blockchain consensus.","major_comments":[],"minor_comments":[{"comment":"The atomic certificate-creation abstraction should be accompanied by an explicit statement that certificates with identical author, round, transactions, and previous references but different endorser lists are semantically equivalent for blockchain generation, so that excluding their co-existence does not under-approximate the set of forking behaviors.","section":"Section 2.8"},{"comment":"The declared type of cmt contains duplicate X and B components; the intended domain seems to be W × (X ∪ B), and this should be corrected in a revision.","section":"Figure 3"},{"comment":"There is a typo 'folllowing' in 'folllowing Narwhal'.","section":"Section 2.8"},{"comment":"The heading 'Anchor Committment' contains a typo; it should be 'Anchor Commitment'.","section":"Section 2.10"},{"comment":"The author name 'Micha? undefinedwiundefinedtek' is corrupted and should be fixed.","section":"Reference [20]"},{"comment":"The label 'rou nd 9' has a stray space.","section":"Figure 6"},{"comment":"The notation B is used both for the set of blocks and for the set of block sequences in the validator state; consider a distinct notation such as B* for sequences to avoid ambiguity.","section":"Section 2.5 and Figure 1"}],"recommendation":"minor_revision","confidential_remarks":"This is a solid paper with a machine-checked central theorem and an appropriately stated trust boundary. The remaining issues are minor and local; I recommend acceptance after minor revisions."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bottom line up front: this is a real result and the reader's report is right. It is the first machine-checked proof I know for nonforking in a DAG-based BFT protocol where the committee changes via stake at every block. The hard part is genuine: the DAG depends on committees, committees depend on the blockchain, and the blockchain depends on the DAG, so the fixed-validator proofs don't compose. The authors break the cycle with a lookback committee and prove the interdependent invariants by simultaneous induction. That is a standard proof technique, not circularity, and ACL2 checks the whole derivation.\n\nCredit where due. The ACL2 artifact is public and substantial—about 20,000 lines with documentation. The paper is honest about the trust boundary: the transition system and the nonforking predicate are trusted, everything else is proved. The generalization from validator counts to stake is also careful: quorum is n-f, not 2f+1, which is the right thing when n is not exactly 3f+1. The theorem is stated for arbitrarily long executions and large states, which is what you want from an inductive invariant proof.\n\nI went looking for under-approximation in the transition rules. The acceptance rule independently checks signer quorum, so faulty-authored certificates can't enter a correct validator's DAG without a quorum. Partial delivery is covered because messages can stay in the network forever. A lagging validator can't disagree about committees because bcmt returns bottom before its blockchain has enough blocks. The simultaneous induction is the right way to handle DAG nonequivocation and committee agreement.\n\nSoft spots, in proportion. The biggest is not in the proof but in the abstract and artifact: the abstract doesn't state the less-than-one-third bound, and no commit hash is pinned for the ACL2 code. Both are easy fixes. The one model abstraction I'd want a sentence about is the atomic endorsement process. Collapsing proposal, endorsement, and certificate creation into one event is safe for safety, because duplicate certificates with the same author and round still require quora and thus intersect in a correct endorser, but the paper doesn't argue this explicitly. Minor.\n\nVerdict: serious referee, yes. This deserves full review and likely acceptance with minor revisions.","headline":"ACL2 machine-checked nonforking proof for dynamic-stake DAG BFT; the model trust boundary is explicit and acceptable, though the abstract and artifact hygiene deserve minor fixes.","tokens_in":38972,"tokens_out":4145,"would_cite":true,"duration_ms":44739,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","68M14"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims a machine-checked proof, in the ACL2 theorem prover, that the blockchains of any two correct validators remain prefix-comparable in every fault-tolerant execution of a DAG-based BFT protocol whose validator set and stake…","keywords":["formal verification","blockchain nonforking","DAG-based BFT consensus","dynamic stake","ACL2","labeled transition system","quorum intersection","inductive invariants"],"falsifier":"Exhibit a sequence of create, accept, advance, and commit events from an initial state such that every active committee has faulty stake below one third, yet two correct validators end with blockchains neither a prefix of the other; the paper's theorem says no such fault-tolerant-reachable state exists. Separately, an implementation-level execution in which a newly bonded validator participates before the lookback delay has elapsed, producing a fork, would show the model omitted a transition relevant to nonforking.","tokens_in":37984,"feed_emoji":"🔗","tokens_out":6058,"duration_ms":65236,"temperature":0.7,"pith_summary":"Blockchain consensus protocols for DAG-based Byzantine fault tolerance usually assume a fixed validator set, but real long-lived chains let validators bond and unbond. This paper claims a formal proof, checked by the ACL2 theorem prover, that a DAG-based BFT protocol with dynamic stake never forks: in every execution where each active validator committee has faulty stake below one third of total stake, the blockchains of any two correct validators are always prefix-comparable. The proof is an inductive invariant proof over a labeled transition system, covering arbitrarily long executions and arbitrarily large states, and it clarifies how the classical less-than-one-third faulty bound generalizes from validator count to validator stake. A sympathetic reader should care because the usual layered correctness arguments do not transfer when DAG and blockchain construction are intertwined through dynamic committees, and an early version of the real protocol did have a fork vulnerability.","feed_headline":"Formal proof: blockchains never fork as validators change","feed_subtitle":"A machine-checked induction shows DAG-based consensus stays fork-free even when the validator set and stake can change every block.","key_machinery":"The labeled state transition system over validator states, DAGs, certificates, messages, and blockchains, with four event kinds: create, accept, advance, and commit. The load-bearing machinery is the family of mutually interdependent inductive invariants, especially certificate nonequivocation, committee agreement, anchor paths, and blockchain redundancy, proved by one simultaneous induction; the quorum threshold is stake-based, with quorum stake defined as total stake minus maximum faulty stake, and a lookback distance delays committee changes so validators can compute the committee for each round from a known blockchain prefix.","core_discovery":"The central claim is that blockchain nonforking for a dynamic-stake DAG BFT protocol can be established by a simultaneous induction over a family of interdependent invariants: certificate nonequivocation, committee agreement, anchor nonforking, blockchain redundancy, and finally blockchain nonforking itself. Because the committee in charge of a round is computed from a blockchain that depends on earlier committees, the proof cannot layer DAG safety over blockchain safety; the paper resolves the apparent circularity by proving the interdependent invariants together for every transition. Fault tolerance enters only through the assumption that each active committee has faulty stake at most the maximum tolerated faulty stake, defined as the largest integer strictly below one third of total stake. Under that assumption, quorum intersection arguments carry over from validator counts to stake, and the paper claims this is the first machine-checked proof of blockchain nonforking for a DAG-based protocol with dynamic stake.","pith_inferences":["Editorial inference: the same interdependent-invariant strategy could probably be reused to prove additional safety properties, such as consistent transaction ordering, but liveness would require adding network delivery or fairness assumptions that the current model deliberately omits.","Editorial inference: the model abstracts validator syncing by treating future validators as already present but inactive, so transferring the guarantee to a real system would require a separate check that the real syncing mechanism cannot create state differences the model hides.","Editorial inference: since the bound is expressed in stake rather than validator count, the result suggests a committee with many faulty validators can still be safe if their combined stake is small; this could be tested by constructing small committees with skewed stake distributions.","Editorial inference: the explicit lookback delay suggests a testable protocol-level requirement that newly bonded validators must not participate in decision-making for at least the lookback number of rounds, and the proof indicates that violating this delay would break the invariant chain."],"forward_implications":["If every active committee satisfies the less-than-one-third faulty-stake bound, then no two correct validators can ever append different blocks to the same prefix; their blockchains differ only by extension.","The guarantee holds even though the committee may be replaced completely in a single block, because the active committee for each round is fixed consistently by the lookback mechanism.","The proof uses the quorum threshold of total stake minus faulty stake rather than the commonly stated 2f+1 bound, so it covers committee sizes where 2f+1 would be insufficient for quorum intersection.","Because the proof is an induction over all reachable states, it applies to arbitrarily long executions and arbitrarily large validator sets, not just to a bounded test scenario.","If the model and its nonforking definition are faithful to an implementation, the result transfers directly to that implementation: no temporary fork can occur under the stated fault tolerance condition."],"supporting_citations":[{"why":"Supplies the DAG construction layer, with certificate creation and broadcast, that the model abstracts into create and accept events.","marker":"[19]"},{"why":"Supplies the anchor-based blockchain construction mechanism where a leader's certificate is voted on by the following round.","marker":"[39]"},{"why":"Supplies the partially synchronous variant of anchor election and commitment that the model's commit rule follows.","marker":"[40]"},{"why":"The theorem prover in which the model, invariants, and proofs are formally checked.","marker":"[22]"},{"why":"The open-source formalization that the paper's claims about machine-checked proofs refer to.","marker":"[14]"},{"why":"Prior machine-checked safety proof for DAG-based protocols with fixed validators; it marks the gap this paper fills for dynamic committees.","marker":"[9]"},{"why":"Earlier machine-checked proof for a fixed-validator DAG protocol, including the observation that formal verification uncovered errors in handwritten proofs.","marker":"[15]"},{"why":"Documents a real fork vulnerability found in an early version of the target protocol, motivating a machine-checkable nonforking proof.","marker":"[45]"}],"fun_headline_variants":["Machine-checked proof: DAG BFT stays fork-free with dynamic stake","Formal proof: dynamic-stake DAG consensus never forks","Verified 1-minute: DAG blockchain nonforking under changing validators","ACL2 proves nonforking for DAG BFT with evolving stake","First machine-checked proof: no forks in dynamic-stake DAG BFT"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"That the ACL2 model faithfully captures the safety-relevant behavior of the real protocol is the load-bearing premise; if a real execution can take a transition the model forbids, or the model permits a behavior that masks a fork, the nonforking theorem does not transfer to the real protocol.","fun_headline_variants_meta":{"raw":{"variants":["Machine-checked proof: DAG BFT stays fork-free with dynamic stake","Formal proof: dynamic-stake DAG consensus never forks","Verified 1-minute: DAG blockchain nonforking under changing validators","ACL2 proves nonforking for DAG BFT with evolving stake","First machine-checked proof: no forks in dynamic-stake DAG BFT"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000417,"raw_usage":{"total_tokens":2146,"prompt_tokens":934,"completion_tokens":1212,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":550,"completion_tokens_details":{"reasoning_tokens":1113}},"tokens_in":550,"tokens_out":1212,"duration_ms":8203,"temperature":1.0,"reasoning_tokens":1113,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T10:54:23.568487+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a sequence of create, accept, advance, and commit events from an initial state such that every active committee has faulty stake below one third, yet two correct validators end with blockchains neither a prefix of the other; the paper's theorem says no such fault-tolerant-reachable state exists. Separately, an implementation-level execution in which a newly bonded validator participates before the lookback delay has elapsed, producing a fork, would show the model omitted a transition relevant to nonforking.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the partially synchronous variant of anchor election and commitment that the model's commit rule follows."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The theorem prover in which the model, invariants, and proofs are formally checked."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The open-source formalization that the paper's claims about machine-checked proofs refer to."},{"cited_title":"Reusable Formal Verification of DAG-based Consensus Protocols","cited_arxiv_id":"2407.02167","evidence_quote":"Prior machine-checked safety proof for DAG-based protocols with fixed validators; it marks the gap this paper fills for dynamic committees."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Documents a real fork vulnerability found in an early version of the target protocol, motivating a machine-checkable nonforking proof."}],"review_version":1}