Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

ChonkyBFT: Consensus Protocol of ZKsync

Bruno França, Denis Kolegov, Igor Konnov, Grzegorz Prusak

TL;DR

ChonkyBFT presents a practical Byzantine fault-tolerant consensus protocol tailored for ZKsync, achieving single-round finality under partial synchrony with $n\ge5f+1$ by combining ideas from FaB Paxos, Fast-HotStuff, and HotStuff-2. It relies on CommitQC and TimeoutQC to guarantee safety and progress, even in the presence of Byzantine leaders or network delays, and includes a re-proposal mechanism to preserve chain consistency. The authors formalize the protocol in Quint, verify safety with inductive invariants, and supplement with model checking via Apalache and randomized simulations, addressing edge cases that often undermine BFT proofs. Empirical evaluation demonstrates scalable performance (up to 100 validators) with competitive block rates and latencies, supported by formal verification to bolster deployment confidence.

Abstract

We present ChonkyBFT, a partially-synchronous Byzantine fault-tolerant (BFT) consensus protocol used in the ZKsync system. The proposed protocol is a hybrid protocol inspired by FAB Paxos, Fast-HotStuff, and HotStuff-2. It is a committee-based protocol with only one round of voting, single slot finality, quadratic communication, and n >= 5f + 1 fault tolerance. This design enables its effective application within the context of the ZKsync rollup, achieving its most critical goals: simplicity, low transaction latency, and reduced system complexity. The target audience for this paper is the ZKsync community and others worldwide who seek assurance in the safety and security of the ZKsync protocols. The described consensus protocol has been implemented, analyzed, and tested using formal methods.

ChonkyBFT: Consensus Protocol of ZKsync

TL;DR

ChonkyBFT presents a practical Byzantine fault-tolerant consensus protocol tailored for ZKsync, achieving single-round finality under partial synchrony with by combining ideas from FaB Paxos, Fast-HotStuff, and HotStuff-2. It relies on CommitQC and TimeoutQC to guarantee safety and progress, even in the presence of Byzantine leaders or network delays, and includes a re-proposal mechanism to preserve chain consistency. The authors formalize the protocol in Quint, verify safety with inductive invariants, and supplement with model checking via Apalache and randomized simulations, addressing edge cases that often undermine BFT proofs. Empirical evaluation demonstrates scalable performance (up to 100 validators) with competitive block rates and latencies, supported by formal verification to bolster deployment confidence.

Abstract

We present ChonkyBFT, a partially-synchronous Byzantine fault-tolerant (BFT) consensus protocol used in the ZKsync system. The proposed protocol is a hybrid protocol inspired by FAB Paxos, Fast-HotStuff, and HotStuff-2. It is a committee-based protocol with only one round of voting, single slot finality, quadratic communication, and n >= 5f + 1 fault tolerance. This design enables its effective application within the context of the ZKsync rollup, achieving its most critical goals: simplicity, low transaction latency, and reduced system complexity. The target audience for this paper is the ZKsync community and others worldwide who seek assurance in the safety and security of the ZKsync protocols. The described consensus protocol has been implemented, analyzed, and tested using formal methods.

Paper Structure

This paper contains 32 sections, 14 theorems, 21 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. ChonkyBFT Overview
  3. Protocol Mechanics: The Happy Path
  4. Handling Unhappy Paths: Timeouts and Re-proposals
  5. Expected Protocol Properties
  6. Basic ChonkyBFT Specification
  7. System Model
  8. Notation
  9. Protocol Specification in Pseudocode
  10. Pseudocode Conventions
  11. Pseudocode Explained
  12. Sending proposals.
  13. Receiving proposals.
  14. Receiving commit votes.
  15. Sending and receiving timeout votes.
  16. ...and 17 more sections

Key Result

Lemma 1

Given two sets $A$ and $B$, from the inequalities $|A| \ge \alpha$, $|B| \ge \beta$, $|A \cup B| \le \gamma$, it follows that $|A \cap B| \ge \alpha + \beta - \gamma$.

Figures (4)

  • Figure 1: The simplest happy path scenario: Replica 0 broadcasts proposal $P_1$; replicas $0, \dots, 4$ receive $P_1$ and broadcast commit votes $C_i$, for $i =0, \dots, 4$; replicas $0, \dots, 4$ receives 5 commit votes $C_0, \dots, C_4$, commits the block and send their new-view votes $N_i$, for $i =0, \dots, 4$. Replica 5 is faulty and ignores all messages.
  • Figure 2: An optimized happy path scenario: Replica 0 broadcasts proposal $P_1$; replicas $0, \dots, 4$ receive $P_1$ and broadcast commit votes $C_i$, for $i =0, \dots, 4$; replica 1 receives 5 commit votes $C_0, \dots, C_4$, commits the block and sends its new-view vote $N_1$; replicas $0, 2, 3, 4$ receive $N_1$, immediately commit the block, and proceed with the next view. Replica 5 is faulty and ignores all messages.
  • Figure 3: An unhappy path scenario: A correct proposer sends a proposal, commit votes are lost owing to asynchrony, all other correct replicas time out.
  • Figure 4: An unhappy path scenario: A faulty replica partitions the correct replica by sending two different proposals. After that, it sends a timeout quorum certificate that contains two subquorums of equal size

Theorems & Definitions (29)

  • Lemma 1
  • proof
  • Corollary 1
  • proof
  • Corollary 2
  • proof
  • Corollary 3
  • Lemma 2
  • proof
  • Definition 1: Invariant $\textsc{LocalHighVote}({v, s, \mathbb{C}})$
  • ...and 19 more