Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Alessandro Coglio, Eric McCarthy

TL;DR

This work provides a formal ACL2 model and machine-checked proof that blockchain nonforking holds for a DAG-based BFT consensus with dynamic stake, where validators can join and leave at every block. By coupling Narwhal-like DAG construction with Bullshark-like blockchain assembly and using a lookback mechanism, the model handles dynamic validator sets and stake-weighted decisions, proving that, under the standard fault-tolerance bound fstk(w) < nstk(w)/3, no two validators’ blockchains diverge beyond a common prefix. The proofs rely on a network of interdependent invariants (DAG nonequivocation, anchor nonforking, signer quorum, committee agreement, and blockchain nonforking) and are executed via ACL2 in under a minute, demonstrating scalability to arbitrarily long executions. The results generalize classical BFT fault-tolerance concepts to dynamic stake-based committees and lay the groundwork for further work on syncing and liveness in such protocols, with open-source ACL2 formalizations available."

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.

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

TL;DR

This work provides a formal ACL2 model and machine-checked proof that blockchain nonforking holds for a DAG-based BFT consensus with dynamic stake, where validators can join and leave at every block. By coupling Narwhal-like DAG construction with Bullshark-like blockchain assembly and using a lookback mechanism, the model handles dynamic validator sets and stake-weighted decisions, proving that, under the standard fault-tolerance bound fstk(w) < nstk(w)/3, no two validators’ blockchains diverge beyond a common prefix. The proofs rely on a network of interdependent invariants (DAG nonequivocation, anchor nonforking, signer quorum, committee agreement, and blockchain nonforking) and are executed via ACL2 in under a minute, demonstrating scalability to arbitrarily long executions. The results generalize classical BFT fault-tolerance concepts to dynamic stake-based committees and lay the groundwork for further work on syncing and liveness in such protocols, with open-source ACL2 formalizations available."

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.

Paper Structure

This paper contains 37 sections, 5 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Formal Model
  3. Labeled State Transition System
  4. Validators
  5. Network
  6. Rounds and Round Advancement
  7. Blockchains
  8. Committees
  9. Certificates and DAGs
  10. Certificate Creation
  11. Certificate Acceptance
  12. Anchor Committment
  13. Execution
  14. Formal Proofs
  15. Formal Model and Proofs in ACL2
  16. ...and 22 more sections

Figures (8)

  • Figure 1: States and Events
  • Figure 2: Transitions
  • Figure 3: Auxiliary Constants, Functions, and Relations
  • Figure 4: Example of Bonded and Active Committees
  • Figure 5: Example DAG of a Validator
  • ...and 3 more figures