bft-voting

BFT Quorum Voting

Models the core voting mechanics that underlie BFT protocols like PBFT, Tendermint, and HotStuff. This is the foundation for understanding why Byzantine consensus works.

Protocol Overview

n nodes (n >= 3f+1)              f faulty nodes can exist

Correct node                     Faulty node
     |                                |
     |-- vote(value) --------------> tally     (votes once)
     |                                |
     |                                |-- vote(A) --> tally  (can vote
     |                                |-- vote(B) --> tally   multiple times)
     |                                |

Value commits when it receives 2f+1 votes from distinct nodes.

Running

make test SPEC=bft-voting
make run SPEC=bft-voting
make verify SPEC=bft-voting

State Variables

Variable	Type	Description
status	Node -> Status	Which nodes are faulty (fixed per run)
votes	Node -> Set[Value]	Votes cast by each node
committed	Set[Value]	Values that reached quorum

Actions

correctVote(node, value)

Correct node casts a vote.

Precondition: Node is correct, hasn't voted yet

Effect: Vote recorded, quorum checked

---

faultyVote(node, value)

Faulty node casts a vote.

Precondition: Node is faulty

Effect: Vote recorded (can accumulate), quorum checked

Safety Properties

agreement

At most one value is ever committed.

committed.size() <= 1

Why it matters: The whole point of BFT - nodes agree despite faulty actors.

---

integrity

Committed values were voted for by some correct node.

committed.forall(v =>
  ALL_NODES.exists(n =>
    status.get(n) == Correct and votes.get(n).contains(v)
  )
)

Why it matters: Faulty nodes alone can't force a commit.

Why It Works

Two quorums of size 2f+1 must overlap by at least f+1 nodes (when n=3f+1). Since at most f nodes are faulty, the overlap contains at least one correct node. Correct nodes vote once, so they can't appear in quorums for different values.

Tests

happyPathTest

All correct nodes vote A, A commits.

equivocationTest

Faulty node votes for both A and B. Agreement still holds.

splitVoteTest

Faulty node tries to split votes. At most one value commits.

Modeling Decisions

Why Synchronous?

We model synchronous communication (votes arrive immediately) to isolate voting mechanics. Async adds complexity without much intuition payoff for the core BFT invariant.

Why Single Round?

A single round captures the essential quorum intersection argument. Multi-round protocols (view changes, locks) build on this foundation.

Next Steps

This spec establishes the foundation. The following specs build on it:

• bft-proposal/ - Add a leader who proposes values
• bft-locking/ - Add locks across multiple rounds
• pbft/ - Full 3-phase protocol

References

• The Byzantine Generals Problem - Lamport, Shostak, Pease (1982)
• PBFT - Castro, Liskov (1999)