← sidechannels

Verification Notes: Raft Consensus Safety in TLA+

Marcus Chen Distributed Systems Lab
· NOTE

The Raft consensus algorithm is designed for understandability, but its formal verification reveals subtle edge cases in leader transition.

Election Safety Invariant

The core safety property of Raft is that at most one leader can be elected in a given term.1 

// TLA+ Specification Snippet: Election Safety Invariant
ElectionSafety ==
    \A t \in Terms :
        Cardinality({i \in Servers : state[i] = Leader /\ currentTerm[i] = t}) <= 1

Using the TLC model checker, we can verify this invariant for small cluster sizes (N=3, N=5).

Log Matching and Persistence

A more complex property is Log Matching: if two logs contain an entry with the same index and term, then the logs are identical.

Liveness and Temporal Logic

While safety is straightforward to prove, liveness requires assumptions about temporal properties.2

References

[1]
Diego Ongaro and John Ousterhout. "In Search of an Understandable Consensus Algorithm". 2014. [PDF]
[2]
Leslie Lamport. "Specifying Systems: The TLA+ Language and Tools". 2002. [PDF]

How to Cite

@article{chen2024raft, title = {Verification Notes: Raft Consensus Safety in TLA+}, author = {Marcus Chen}, year = {2024}, url = {https://sidechannels.pub/posts/raft-verification-tla/} }