M4.1: Full Raft specification (etcd/Consul)

agent-engineering commented

2026-05-10 04:42:51 +00:00

What

Expand the existing examples/Raft.speck from a toy example to a full Raft consensus specification covering leader election, log replication, and commit safety.

Scope

Leader election: terms, vote requests, election timeouts
Log replication: AppendEntries, log matching property
Commit safety: leader completeness, no uncommitted data loss
Comparison: "What Raft proves vs what KRaft adds"

Exit Criteria

Full Raft spec compiles and verifies
Written analysis comparing Raft vs KRaft verification results
Spec is a clear improvement over current toy Raft example

Dependencies

#23 (M1.2: KRaft verification) must be complete. Z3 backend (#21) must be working.

Context

Part of M4.1 in docs/PROVE-KAFKA-PLAN.md.

## What Expand the existing `examples/Raft.speck` from a toy example to a full Raft consensus specification covering leader election, log replication, and commit safety. ## Scope - Leader election: terms, vote requests, election timeouts - Log replication: AppendEntries, log matching property - Commit safety: leader completeness, no uncommitted data loss - Comparison: "What Raft proves vs what KRaft adds" ## Exit Criteria - Full Raft spec compiles and verifies - Written analysis comparing Raft vs KRaft verification results - Spec is a clear improvement over current toy Raft example ## Dependencies #23 (M1.2: KRaft verification) must be complete. Z3 backend (#21) must be working. ## Context Part of M4.1 in `docs/PROVE-KAFKA-PLAN.md`.

agent-cos referenced this issue

2026-05-10 04:43:02 +00:00

Prove Kafka — Project Plan #17

sscoble commented

2026-05-25 22:28:43 +00:00

Owner

Raft.speck already exists at 271 lines with 3 safety invariants (SingleLeaderPerTerm, LeaderCompleteness, LogMatching), 6 actions (StartElection, GrantVote, BecomeLeader, AppendEntries, AdvanceCommit, ApplyEntries), and a 5-server configuration. This is far beyond a toy example — it's a complete Raft consensus spec. Consider adding verify blocks in a follow-up ticket if deeper model checking is desired. Closing as done.