Pith. sign in

REVIEW 7 minor 46 references

Formal Verification of Blockchain Nonforking in DAG-Based BFT Consensus with Dynamic Stake

T0 review · 0 major / 7 minor · reviewed 2026-08-16 · deepseek-v4-flash

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

Pith's one-line read 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…

desk verdict 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. read the letter →

arxiv 2504.16853 v1 pith:5RWBA7DU submitted 2025-04-23 cs.LO

Alessandro Coglio , Eric McCarthy This is my paper · ORCID
classification cs.LO MSC 68Q6068M14
keywords formalverificationblockchainnonforkingDAG-basedBFTconsensusdynamicstakeACL2labeledtransitionsystemquorumintersectioninductiveinvariants
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

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

0 major / 7 minor

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.

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.

minor comments (7)
  1. [Section 2.8] 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.
  2. [Figure 3] 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.
  3. [Section 2.8] There is a typo 'folllowing' in 'folllowing Narwhal'.
  4. [Section 2.10] The heading 'Anchor Committment' contains a typo; it should be 'Anchor Commitment'.
  5. [Reference [20]] The author name 'Micha? undefinedwiundefinedtek' is corrupted and should be fixed.
  6. [Figure 6] The label 'rou nd 9' has a stray space.
  7. [Section 2.5 and Figure 1] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the blockchain nonforking theorem is an independently machine-checked invariant proof, with the acknowledged model-adequacy boundary being a standard limitation rather than a circular step.

full rationale

I found no circular step in the claimed derivation. The central claim is a machine-checked ACL2 invariant proof that blockchains never fork in the formal labeled transition system, under a fault-tolerance assumption on each arising active committee. The nonforking property is not baked into the definitions: the transition rules explicitly allow faulty validators to create arbitrary or equivocal certificates, allow messages to remain undelivered forever, and allow deadlocked executions, so forking behaviors are representable in the model; nonforking holds only on the subset of fault-tolerant-reachable states, as a proved consequence of a chain of invariants. The apparent mutual dependency among DAG nonequivocation, committee agreement, and blockchain nonforking is explicitly addressed as a simultaneous induction over interdependent invariants (Section 3 and Appendix B), which is a standard and valid proof technique rather than a circular derivation. No parameter is fitted to data and then presented as a prediction; no uniqueness theorem from prior work by these authors is imported to force a choice; and the only self-citation, the open-source ACL2 artifact [14], is a code artifact supporting reproducibility, not a load-bearing mathematical premise. The paper's own statement that the ACL2 transition system and the blockchain nonforking predicate are trusted to adequately capture the protocol is a clearly acknowledged model-adequacy trust boundary, which is a limitation of the formalization's scope, not a circularity in the proof of the theorem about the model itself.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The proof is parametric in the uninterpreted constants (lookback, genesis committee, leader function, certificate order), so there are no fitted numbers. The domain assumptions are standard for BFT consensus models. No new entities are postulated beyond the protocol's own concepts.

assumptions (5)
  • domain assumption Cryptographic signatures are unforgeable: a certificate's author and endorsers are exactly the validators whose signatures it carries.
    Section 2.7 states that faulty validators cannot forge signatures of correct validators; the model relies on this to identify authors and endorsers.
  • domain assumption The set of correct validators D(v) is fixed across the execution; future validators are modeled as present but inactive until they bond.
    Section 2.2 notes that new validators sync their state before participating, so the model pretends all future correct validators are already in the system.
  • domain assumption The network provides authenticated point-to-point links with unbounded delays; messages may be delivered arbitrarily late or never.
    Section 2.3 explicitly adopts this standard asynchronous network model from the BFT literature.
  • domain assumption The protocol parameters lkbk (lookback), gcmt (genesis committee), leader, and orderCert are uninterpreted constants or functions satisfying only the stated constraints.
    Figure 3 leaves these undefined: lkbk is a positive integer, gcmt is a committee, leader returns a member of a non-empty committee, and orderCert orders a set without repetition. The proof is schematic over these choices.
  • domain assumption All transactions, including bonding and unbonding, are valid and do not need further validation.
    Section 2.5, footnote 4, says the model keeps all transactions valid for simplicity, as this does not affect the nonforking property.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formal Verification of Blockchain Nonforking in DAG-Based BFT Consensus with Dynamic Stake." pith.science (2026). https://pith.science/paper/5RWBA7DU

@misc{pith2026250416853,
  author       = {Pith},
  title        = {Pith review of: Formal Verification of Blockchain Nonforking in DAG-Based BFT Consensus with Dynamic Stake},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/5RWBA7DU}},
  note         = {Machine review of arXiv:2504.16853}
}
read the original abstract

Blockchain consensus protocols enable participants to agree on consistent views of the blockchain that may be ahead or behind relative to each other but do not fork into different chains. A number of recently popular Byzantine-fault-tolerant (BFT) protocols first construct a directed acyclic graph (DAG) that partially orders transactions, then linearize the DAG into a blockchain that totally orders transactions. The definitions and correctness proofs of these DAG-based protocols typically assume that the set of participants is fixed, which is impractical in long-lived blockchains. Additionally, only a few of those proofs have been machine-checked, uncovering errors in some published proofs. We developed a formal model of a DAG-based BFT protocol with dynamic stake, where participants can join and leave at every block, with stake used to weigh decisions in the protocol. We formally proved that blockchains never fork in the model, also clarifying how BFT bounds on faulty participants generalize to these highly dynamic sets of participants. Our model and proofs are formalized in the ACL2 theorem prover, apply to arbitrarily long executions and arbitrarily large system states, and are verified in 1 minute by ACL2.

Figures

Figures reproduced from arXiv: 2504.16853 by the authors.

Figure 1
Figure 1. States and Events 2.1 Labeled State Transition System The labeled state transition system is the tuple hS, E, I, T i, where S is the set of states, E is the set of events, I ⊆ S is the set of initial states, and T ⊆ S×E×S is the transition relation among old states, events, and new states. T (s, e, s′ ) holds exactly when the event e causes a transition from the old state s to the new state s ′ . The execution relat… view at source ↗
Figure 2
Figure 2. Transitions 4 [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Auxiliary Constants, Functions, and Relations [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (10 more)
Figure 1
Figure 1. Figure 1: As described later, blocks are generated only at (s [PITH_FULL_IMAGE:figures/full_fig_p007_1.png]
Figure 4
Figure 4. Figure 4: Example of Bonded and Active Committees [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: Example DAG of a Validator A certificate c ∈ C includes the address a of its author, i.e. the validator who created the certificate. In our model, this a represents a cryptographic signature with the validator’s private key. Certificate authors can be thus relied upon:…
Figure 6
Figure 6. Figure 6: Example of Committed and Skipped Anchors [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 2
Figure 2. Figure 2: As DAGs are constructed, blocks may be generated. A [PITH_FULL_IMAGE:figures/full_fig_p013_2.png]
Figure 3
Figure 3. Figure 3: If S1, . . . , Sn are sets, with n ≥ 2, then S1 × · · · × Sn is their Cartesian product, i.e. the set of all n-tuples hα1, . . . , αni, where each αi ∈ Si . If S is a set, Se is the set of all finite subsets of S. For example, Mf in [PITH_FULL_IMAGE:figures/full_fig_p…
Figure 2
Figure 2. Figure 2: If µ is a finite map and S ⊆ D(µ), µ ↓S is the restriction of µ to S ⊆ D(µ), i.e. the finite map whose domain is S and that maps each α ∈ S to µ(α). For example, w↓D(w)\{a} in the definition of cmt in [PITH_FULL_IMAGE:figures/full_fig_p017_2.png]
Figure 7
Figure 7. Figure 7: Invariants B Invariants and Proof Sketches [PITH_FULL_IMAGE:figures/full_fig_p018_7.png]
Figure 8
Figure 8. Figure 8: Additional Auxiliary Sets, Functions, and Relati [PITH_FULL_IMAGE:figures/full_fig_p019_8.png]
Figure 8
Figure 8. Figure 8: the latter consist of the certificates in all the DAG [PITH_FULL_IMAGE:figures/full_fig_p020_8.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

46 extracted references · 28 canonical work pages

  1. [1]

    The Aleo Blockchain

    Aleo 2024. The Aleo Blockchain. https://aleo.org

    work page 2024

  2. [2]

    Aleo Team and Provable Team. 2019. snarkOS. https://github.com/AleoNet/snarkOS

    work page 2019

  3. [3]

    Aleo Team and Provable Team. 2020. snarkVM. https://github.com/AleoNet/snarkVM

    work page 2020

  4. [4]

    Alturki, Jing Chen, Victor Luchangco, Brandon M oore, Karl Palmskog, Lucas Peña, and Grigore Roşu

    Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M oore, Karl Palmskog, Lucas Peña, and Grigore Roşu. 2020. Towards a Verified Model of the Algorand Consensus Protocol in Coq. Springer International Publishing, 362–367. https://doi.org/10.1007/978-3-030-54994-7_27

    work page doi:10.1007/978-3-030-54994-7_27 2020

  5. [5]

    Balaji Arun, Zekun Li, Florian Suri-Payer, Sourav Das, a nd Alexander Spiegelman. 2024. Shoal++: High Throughput DAG BFT Can Be Fast! arXiv:2405.20 488 [cs.DC] https://arxiv.org/abs/2405.20488

    arXiv 2024

  6. [6]

    Jeremy A vigad and Richard Zach. 2016. The Epsilon Calcul us. In The Stanford Encyclopedia of Phi- losophy (summer 2016 ed.), Edward N. Zalta (Ed.). Metaphysics Resea rch Lab, Stanford University. https://plato.stanford.edu/archives/sum2016/entries/epsilon-calculus/

    work page 2016

  7. [7]

    Kushal Babel, Andrey Chursin, George Danezis, Anastasi os Kichidis, Lefteris Kokoris-Kogias, Arun Koshy, Alberto Sonnino, and Mingwei Tian. 2024. Mysticeti: Reaching the Limits of Latency with Uncertified DAGs. arXiv:2310.14821v4 [cs.DC] https://arxiv.org/abs/2310.14821v4

    arXiv 2024

  8. [8]

    Leemon Baird. 2016. The Swirlds hashgraph consensus algorithm: Fair, fast, Byzant ine fault tolerance . Technical Report SWIRLDS-TR-2016-01. Swirlds Inc. Revisi on date: March 18, 2018

    work page 2016

Show all 46 references
  1. [9]

    Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernh ard Scholz, and Pavle Subotic. 2024. Reusable Formal Verification of DAG-based Consensus Protoc ols. arXiv:2407.02167v1 [cs.LO] https://arxiv.org/abs/2407.02167v1

    2024 arXiv

  2. [10]

    Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Mari jana Lazić, Pierre Tholoniat, and Josef Widder. 2022. Holistic Verification of Blockchain Consensu s. arXiv:2206.04489 [cs.CR] https://arxiv.org/abs/2206.04489

    2022 arXiv

  3. [11]

    Boyer and J Strother Moore

    Robert S. Boyer and J Strother Moore. 1979. The Boyer-Moore Theorem Prover . Academic Press. https://www.cs.utexas.edu/users/boyer/ftp/nqthm/. 31

    1979

  4. [12]

    Harold Carr, Christopher Jenkins, Mark Moir, Victor Ca cciari Miraldo, and Lisandra Silva. 2022. To- wards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version. arXiv:2203.14711v2 [cs.DC] https://arxiv.org/abs/2203.14711v2

    2022 arXiv

  5. [13]

    Sang-Min Choi, Jiho Park, Quan Nguyen, Andre Cronje, Ki young Jang, Hyunjoon Cheon, Yo-Sub Han, and Byung-Ik Ahn. 2018. OPERA: Reasoning about continuous c ommon knowledge in asynchronous distributed systems. arXiv:1810.02186 [cs.DC] https://arxiv.org/abs/1810.02186

    2018 arXiv

  6. [14]

    Alessandro Coglio and Eric McCarthy. [n. d.]. ACL2 Form al Model and Proofs of AleoBFT. https://github.com/acl2/acl2/tree/master/books/projects/aleo/bft

  7. [15]

    Karl Crary. 2021. Verifying the Hashgraph Consensus Al gorithm. arXiv:2102.01167 [cs.LO] https://arxiv.org/abs/2102.01167

    2021

  8. [16]

    Xiaohai Dai, Guanxiong Wang, Jiang Xiao, Zhengxuan Guo , Rui Hao, Xia Xie, and Hai Jin. 2024. LightDAG: A Low-latency DAG-based BFT Consensus through Li ghtweight Broadcast. Cryptology ePrint Archive, Paper 2024/160. https://eprint.iacr.org/2024/160

    2024

  9. [17]

    Xiaohai Dai, Zhaonan Zhang, Jiang Xiao, Jingtao Yue, Xi a Xie, and Hai Jin. 2024. GradedDAG: An Asynchronous DAG-based BFT Consensus with Lower Latency . Cryptology ePrint Archive, Paper 2024/142. https://eprint.iacr.org/2024/142

    2024

  10. [18]

    George Danezis and David Hrycyszyn. 2018. Blockmania: from Block DAGs to Consensus. arXiv:1809.01620v2 [cs.CR] https://arxiv.org/abs/1809.01620v2

    2018 arXiv

  11. [19]

    George Danezis, Eleftherios Kokoris Kogias, Alberto S onnino, and Alexander Spiegelman. 2022. Nar- whal and Tusk: A DAG-based Mempool and Efficient BFT Consensus . arXiv:2105.11827v4 [cs.CR] https://arxiv.org/abs/2105.11827v4

    2022 arXiv

  12. [20]

    Adam Gągol, Damian Leśniak, Damian Straszak, and Micha ł undefinedwiundefinedtek. 2019. Aleph: Efficient Atomic Broadcast in Asynchronous Networks w ith Byzantine Nodes. In Pro- ceedings of the 1st ACM Conference on Advances in Financial T echnologies (Zurich, Switzer- land) (AFT ...

    2019

  13. [21]

    Philipp Jovanovic, Lefteris Kokoris Kogias, Bryan Kum ara, Alberto Sonnino, Pasindu Tennage, and Igor Zablotchi. 2024. Mahi-Mahi: Low-Latency Asynchro nous BFT DAG-Based Consensus. arXiv:2410.08670v2 [cs.DC] https://arxiv.org/abs/2410.08670v2

    2024 arXiv

  14. [22]

    Matt Kaufmann and J Strother Moore. 1990. The ACL2 Theor em Prover: Web Site. http://acl2.org

    1990

  15. [23]

    Idit Keidar, Eleftherios Kokoris-Kogias, Oded Naor, a nd Alexander Spiegelman. 2021. All You Need is DAG. arXiv:2102.08325 [cs.DC] https://arxiv.org/abs/2102.08325

    2021 arXiv

  16. [24]

    Idit Keidar, Oded Naor, Ouri Poupko, and Ehud Shapiro. 2 023. Cordial Miners: Fast and Efficient Consensus for Every Eventuality. In 37th International Symposium on Distributed Computing (DISC 2023) . Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIP...

    2023 doi

  17. [25]

    Liu, Saksham Chand, and Scott D

    Yanhong A. Liu, Saksham Chand, and Scott D. Stoller. 201 9. Moderately Complex Paxos Made Sim- ple: High-Level Executable Specification of Distributed Al gorithms. In Proceedings of the 21st Inter- national Symposium on Principles and Practice of Declarativ e Programming (PPDP ...

  18. [26]

    Liu and Scott D

    Yanhong A. Liu and Scott D. Stoller. 2024. Tutorial: Con sensus Algorithms from Classical to Blockchain: Quickly Program, Configure, Run, a nd Check. In 2024 IEEE 44th International Conference on Distributed Computing Syste ms Workshops (ICDCSW) . 1–4. https://doi.org/10.1109/I...

    2024

  19. [27]

    Giuliano Losa. 2021. Formally Verifying the Tendermint Blockchain Protocol . Technical Report. Galois. https://galois.com/blog/2021/07/formally-verifying- the-tendermint-blockchain-protocol/ Accessed: 2024-11-01

    2021

  20. [28]

    Giuliano Losa and Mike Dodds. 2020. On the Formal Verific ation of the Stellar Consensus Protocol. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) (Op en Access Series in Informatics (OASIcs), Vol. 84) , Bruno Bernardo and Diego Marmsoler (Eds.). Schloss Dagstu hl...

    2020 doi

  21. [29]

    Dahlia Malkhi, Chrysoula Stathakopoulou, and Maofan Y in. 2024. BBCA-CHAIN: Low Latency, High Throughput BFT Consensus on a DAG. arXiv:2310 .06335 [cs.DC] https://arxiv.org/abs/2310.06335

    2024 arXiv

  22. [30]

    Dahlia Malkhi and Pawel Szalachowski. 2022. Maximal Ex tractable Value (MEV) Protection on a DAG. arXiv:2208.00940v4 [cs.CR] https://arxiv.org/abs/2208.00940v4

    2022 arXiv

  23. [31]

    Satoshi Nakamoto. 2008. Bitcoin: A Peer-to-Peer Elect ronic Cash System

    2008

  24. [32]

    Quan Nguyen, Andre Cronje, Michael Kong, Egor Lysenko, and Alex Guzev. 2021. Lachesis: Scalable Asynchronous BFT on DAG Streams. arXiv:2108.01900 [cs.DC] https://arxiv.org/abs/2108.01900

    2021 arXiv

  25. [33]

    Praveen, Raghavendra Ramesh, and Isaac Doidge

    M. Praveen, Raghavendra Ramesh, and Isaac Doidge. 2024 . Formally Verifying the Safety of Pipelined Moonshot Consensus Protocol. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024) (Open Access Series in Informatics (OASIcs), Vol. 11 8), Bruno Bernardo ...

    2024 doi

  26. [34]

    Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Es teves Veríssimo. 2018. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In European Symposium on Programming . https://api.semanticscholar.org/CorpusID:4899635

    2018

  27. [35]

    Sean Rowan and Na iri Usher. 2019. Flare Consensus Proto col. https://flare.network/wp-content/uploads/FCP-White- Paper.pdf

    2019

  28. [36]

    Schett and George Danezis

    Maria A. Schett and George Danezis. 2021. Embedding a De terministic BFT Protocol in a Block DAG. In Proceedings of the 2021 ACM Symposium on Principles of Distrib uted Computing (Vir- tual Event, Italy) (PODC’21). Association for Computing Machinery, New York, NY, USA, 17 7–1...

    2021

  29. [37]

    Nibesh Shrestha, Rohan Shrothrium, Aniket Kate, and Ka rtik Nayak. 2024. Sailfish: To- wards Improving the Latency of DAG-based BFT. Cryptology eP rint Archive, Paper 2024/472. https://eprint.iacr.org/2024/472

    2024

  30. [38]

    Alexander Spiegelman, Balaji Arun, Rati Gelashvili, a nd Zekun Li. 2023. Shoal: Improving DAG-BFT Latency And Robustness. arXiv:2306.03058v2 [cs.DC] https://arxiv.org/abs/2306.03058v2

    2023 arXiv

  31. [40]

    Alexander Spiegelman, Neil Giridharan, Alberto Sonni no, and Lefteris Kokoris-Kogias

  32. [41]

    Chrysoula Stathakopoulou, Michael Wei, Maofan Yin, Ho ngbo Zhang, and Dahlia Malkhi. 2023. BBCA-LEDGER: High Throughput Consensus meets Low Latency. arXiv:2306.14757 [cs.DC] https://arxiv.org/abs/2306.14757

    2023 arXiv

  33. [42]

    arXiv :2209.05633v1 [cs.DC] https://arxiv.org/abs/2209.05633v1

    Bullshark: The Partially Synchronous Version. arXiv :2209.05633v1 [cs.DC] https://arxiv.org/abs/2209.05633v1

    arXiv

  34. [43]

    Sol Swords and Jared Davis. 2015. Fix Your Types. In Proc. 13th International Workshop on the ACL2 Theorem Prover and Its Applications

    2015

  35. [44]

    Guy L. Steele. 1984. Common Lisp the Language . Digital Press. 33

    1984

  36. [45]

    zkSecurity. 2023. Audit of Aleo’s consensus. https://www.zksecurity.xyz/reports/aleo-consensus 34

    2023

  37. [46]

    Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, S eth Gilbert, and Ilya Sergey. 2024. Compositional Verification of Composite Byzantine Protocols. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security (Salt Lake City, UT, USA) (CCS ’24)...

    2024

  38. [2022]

    arXiv:2 201.05677v3 [cs.CR] https://arxiv.org/abs/2201.05677v3

    Bullshark: DAG BFT Protocols Made Practical. arXiv:2 201.05677v3 [cs.CR] https://arxiv.org/abs/2201.05677v3

    arXiv

Pith tools

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