Raft

Honest by Construction

Raft leaders, votes, state, and commit are recomputed from events.

highlighted = computed this step

Honest by construction

The author supplies initial follower preconditions and ordered events. The engine rejects authored initial leaders and commits, then recomputes state from events. Note: expected facts can reject a mismatch but cannot create the answer.

honest raft\text{honest raft}

Compiled replay

The compiled trace has 1 leader and commitIndex 1. Note: both facts fall out of replay.

leaders=1,commitIndex=1\text{leaders}=1,\quad \text{commitIndex}=1

a simplified Raft over a tiny cluster: terms, votes, leader election, and the term-restricted commit rule are exact on these traces; the full safety proof, membership changes, snapshotting, log compaction, and real RPC/timing are beyond these traces - no product claims.

Honest Raft commitIndex 1 0 1 2 3 4 A t0/F t1/C t1/L t1/L t1/L B t0/F t1/F t1/F t1/F t1/F C t0/F t1/F t1/F t1/F t1/F vote tally t1 A:3 leader log A t1:x

Wrong result reject

A wrong expected commitIndex and an authored initial leader are rejected in the lesson self-test. Note: no inconsistent Raft state can become the rendered answer.

reject mismatch\text{reject mismatch}

Summary

The Databases and Transactions track is complete: nine books of exact, recomputed database behavior. Note: this is simplified Raft; the full safety proof, membership changes, snapshots, and real timing are beyond these traces.

track complete\text{track complete}