bft-locking

BFT with Multi-Round Locking

Extends bft-proposal with multiple rounds and locking. Demonstrates why locking is essential for safety across view changes.

Protocol Overview

Round 0                          Round 1
  |                                |
  |  A gets quorum (commits)       |  New leader proposes B
  |  Nodes lock on A               |
  |                                |  Locked nodes vote A (not B)
  |                                |  B cannot reach quorum
  |                                |
  v                                v

The Problem Without Locking:
  Round 0: A commits with {N1, N2, N3}
  Round 1: B could commit with {N1, N3, N4} if N3 "forgets" it voted A

Locking prevents this: N2, N3 are locked on A and cannot vote B.

Running

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

State Variables

Variable	Type	Description
status	Node -> Status	Which nodes are faulty
round	Round	Current round number
leader	Round -> Node	Leader for each round
locked	Node -> Lock	What each node is locked on
votes	Node -> Value	Votes cast this round
committed	Set[Value]	Values committed (all rounds)

Actions

correctVote(node, value)

Correct node votes for a value.

Precondition: Node is correct, hasn't voted this round

Constraint: If locked, must vote for locked value

Effect: Vote recorded, may trigger commit

---

faultyVote(node, value)

Faulty node votes for any value (ignores locks).

Precondition: Node is faulty

Effect: Vote recorded, may trigger commit

---

observeQuorum(node, value)

Node sees quorum for a value and locks on it.

Precondition: Node is correct, value has quorum

Effect: Node locks on value at current round

---

nextRound

Advance to next round (e.g., leader timeout).

Effect: Round increments, votes cleared, locks preserved

Safety Properties

agreement

At most one value commits across all rounds.

committed.size() <= 1

Key Insight: Why Locking?

Without locking, this attack is possible:

1. Round 0: A gets quorum {N1, N2, N3}, commits
2. Round 1: Faulty N1 votes B, correct N3 and N4 vote B
3. Result: B commits with {N1, N3, N4} - agreement violated!

With locking:

• N2, N3 saw A reach quorum → they lock on A
• In round 1, N2 and N3 can only vote A
• B can get at most 2 votes (N1 + N4) → no quorum

The Lock Rule

A correct node that sees 2f+1 votes for value V in round R:

1. Locks on (V, R)
2. In all future rounds, can only vote for V (until unlocked by higher-round evidence)

This ensures: if V commits, no other value can reach quorum in any round.

Tests

lockPreventsConflictTest

A commits in round 0. Locked nodes prevent B from committing in round 1.

whyLockingMattersTest

Shows the attack scenario that locking prevents.

latecomerTest

Node that missed round 0 can vote differently in round 1, but locks still protect agreement.

Next Steps

• pbft/ - Full 3-phase protocol combining all concepts

References

• bft-voting/ - BFT quorum voting
• bft-proposal/ - BFT with leader proposal
• Tendermint - BFT with locking