Consensus · MoonBit · WebAssembly
A cluster that stays
in agreement -
even when it shouldn't.▊
Raft is how replicated systems keep one true log through crashes, partitions, and dropped mail. This is a faithful MoonBit port of etcd's raft - the same protocol behind etcd, TiKV and Consul - with the algebra of the language doing work the Go original left to convention. It's all on GitHub.
Every committed entry is agreed by a majority before it counts. The term stamp (t1..t3) records which leadership era wrote it - the ordering key that makes the log a single, undisputed history.
What it covers
A complete Raft, not a sketch
Election, replication, membership, persistence, reads - the parts most teaching implementations skip are the parts that decide correctness under failure. All of it is here, and all of it is tested.
Leader election
Follower / Candidate / Leader roles, the up-to-date-log voting restriction (§5.4.1), pre-vote so a partitioned node can't inflate the term, and randomized timeouts off a per-node PRNG.
Log replication
AppendEntries with the log-matching check, conflicting-suffix
truncation, one-jump backoff via conflict_index, and
per-follower progress (probe / replicate / snapshot).
Membership & joint consensus
Single-server add/remove and full C(old,new) joint consensus (§6),
carried as ConfChange entries and folded in by a
configuration state machine.
Persistence & recovery
A HardState, an append-only write-ahead log with
replay, and an etcd-style MemoryStorage engine with
compaction, snapshots and a storage-backed recovery path.
Reads & transfer
Linearizable ReadIndex / leader-lease reads, check-quorum so a
cut-off leader steps down, and orderly leadership transfer via
TimeoutNow (§3.10).
Deterministic chaos
A single-seed simulator that drops, delays, reorders, partitions and crashes nodes - with built-in checks for the Raft safety invariants and a full chaos suite.
Why this one
The types did the auditing
Porting from Go was not transcription. Three independent methods - transliteration against the 258 upstream tests, an adversarial falsification audit, and a Go-versus-MoonBit differential trace - surfaced 24 real defects, each fixed under a red-then-green regression test. MoonBit's algebraic data types and exhaustive matching turned a class of them into compile-time-visible cases - including one that could elect two leaders in a single term.
B1 Two leaders, one term
A reordered, stale VoteResp was being counted into a
false majority. Replacing the term check with an exhaustive
TermRel match made "message from an older term" a case
you cannot forget to handle. Election Safety restored.
Read the write-up →
S2 Compacted vs. unavailable
The old storage returned the same None for "index was
compacted away" and "index past the end" - so a caller couldn't
tell whether to snapshot or wait. A StorageError ADT
made the two states impossible to conflate.
Read the write-up →
See for yourself
Real consensus, running in your browser
The demo isn't a JavaScript re-implementation and isn't a
single-threaded animation. Each of the five nodes is a separate
WebAssembly instance in its own Web Worker, ticking on its own timer,
exchanging messages through postMessage - genuinely
concurrent, genuinely non-deterministic. Cut the network and watch two
terms diverge; heal it and watch them reconcile.