` 26 D. Mazieres hence vote to conﬁrm) contradictory statements, this means that for a given ⟨V,Q⟩, Theorem 5 ensures a set S of well-behaved nodes cannot externalize contradictory values so long as S enjoys quorum intersection despite V⧵S. This safety holds if V and Qchangeonlybetweenslots,butwhatiftheychangemid-slot(forinstance,inreaction to node crashes)? To reason about safety under reconﬁguration, we join all old and new quorum slice sets, reﬂecting the fact that nodes may make decisions based on a combination of mes- sages from different conﬁguration eras. To be very conservative, we might require quorum intersection of the aggregation of the present conﬁguration with every past conﬁguration. However, we can relax this slightly by separating nodes that have sent illegal messages from those that have merely crashed. THEOREM13. Let ⟨V ,Q ⟩,…,⟨V ,Q ⟩ be the set of conﬁgurations an FBAS has 1 1 k k experienced during agreement on a single slot. Let V = V ∪ ⋯ ∪ V and Q(v) = {q ∣ 1 k ∃j such that v ∈ V ∧ q ∈ Q (v)}. Let B ⊆ V be a set such that B contains all ill- j j behaved nodes that have sent illegal messages, though V⧵B may still contain crashed (unresponsive) nodes. Suppose nodes v and v are well-behaved, v externalizes x for 1 2 1 1 the slot, and v externalizes x . If ⟨V,Q⟩B enjoys quorum intersection, then x = x . 2 2 1 2 PROOF. For v to externalize x , it must have ratiﬁed accept(commit ⟨n ,x ⟩) in col- 1 1 1 1 laboration with a pseudo-quorum U ⊆ V. We say pseudo-quorum because U might 1 1 not be a quorum in ⟨V ,Q ⟩ for any particular j, as ratiﬁcation may have involved j j messages spanning multiple conﬁgurations. Nonetheless, for ratiﬁcation to succeed ∀v ∈ U ,∃j,∃q ∈ Q (v) such that q ⊆ U . It follows from the construction of Q that 1 j 1 q ∈ Q(v). Hence U is a quorum in ⟨V,Q⟩. By a similar argument a pseudo-quorum 1 U musthave ratiﬁed accept(commit ⟨n ,x ⟩), and U must be a quorum in ⟨V,Q⟩. By 2 2 2 2 B quorumintersection of ⟨V,Q⟩ , there must exist some v ∈ V⧵B such that v ∈ U ∩U . 1 2 By assumption, such a v ∉ B could not claim to accept incompatible ballots. Since v conﬁrmedacceptingcommitforballotswithbothx andx ,itmustbethatx =x . 1 2 1 2 For liveness of a node v, we care about several things when an FBAS has undergone a series of reconﬁgurations ⟨V ,Q ⟩,…,⟨V ,Q ⟩ within a single slot. First, the safety 1 1 k k prerequisites of Theorem 13 must hold for v and the set of nodes v cares about, since violating safety undermines liveness and Theorem 11 requires quorum intersection. Second,thesetofill-behavednodesinthelateststate,⟨V ,Q ⟩,mustnotbev-blocking, k k as this could deny v a quorum and prevent it from ratifying statements. Finally, v’s state must never have been poisoned by a v-blocking set falsely claiming to accept a statement. To summarize, then, if B is the set of nodes that have sent illegal messages, we consider a node v to be cumulatively intact when the following conditions hold: (1) v is intact in the latest conﬁguration ⟨V ,Q ⟩, k k (2) The aggregation of the present and all past conﬁgurations has quorum intersec- tion despite B (i.e., the prerequisite for Theorem 13 holds), and (3) B is not v-blocking in ⟨V ,Q ⟩ for any 1 ≤ j ≤ k. j j The next few theorems show that ill-behaved nodes cannot drive intact nodes into dead-end stuck states: THEOREM14. In an FBAS with quorum intersection, if no intact node is in the EXTERNALIZE phase and an intact node with ballot ⟨n,x⟩ arms its timer as described in Section 6.2.2, then, given sufﬁcient communication, every intact node v can set bv ≥ n before any timer ﬁres.

The Stellar Consensus Protocol Page 26 Page 28