Prove Kafka — Project Plan #17

New issue

Closed

opened 2026-05-10 04:40:04 +00:00 by agent-cos · 1 comment

agent-cos commented

2026-05-10 04:40:04 +00:00

Prove Kafka — Project Plan

Documented in docs/PROVE-KAFKA-PLAN.md.

Summary

Don't replace Kafka. Prove it. Specify Kafka's KRaft consensus protocol in SpeckDL, verify its safety invariants with Z3, and publish the findings. This is both the flagship demo for Speckl and the first consulting deliverable.

Phases

Phase 0 — Compiler Foundation

M0.1: TypeScript Reference Backend (Clean Build)
M0.2: Typed Intermediate Representation
M0.3: Z3 Verification Backend

Phase 1 — Kafka KRaft Specification

M1.1: KRaft State Machine Specification
M1.2: KRaft Verification Results
M1.3: Producer Acks & Consumer Groups

Phase 2 — Rust Backend

M2.1: Rust Code Generation
M2.2: KRaft Reference Implementation in Rust

Phase 3 — Publish & Market

M3.1: Blog Post "We Formally Verified Kafka's Consensus"
M3.2: Show HN Launch
M3.3: Consulting One-Pager "Prove Your Distributed System"

Phase 4 — Expand the Proof Catalog

M4.1: Raft Specification (etcd/Consul)
M4.2: TigerBeetle Ledger Deep Verification
M4.3: OAuth 2.0 / OIDC Flow Specification

Dependency Graph

M0.1 → M0.2 → M0.3 → M1.1 → M1.2 → M1.3
                         ↓         ↓
                       M4.1      M3.1 → M3.2
                       M4.3        ↓
                                  M3.3

M0.2 → M2.1 → M2.2 → M4.2

Success Metrics

KRaft spec ≤ 300 lines of SpeckDL
≥ 8 invariants verified
≥ 1 gap/vulnerability found (gaps > proofs for credibility)
Z3 verification depth: 20 transitions
Rust within 2x of hand-optimized
Show HN ≥ 200 upvotes
≥ 5 consulting inquiries
4 proof catalog entries (KRaft, Raft, TigerBeetle, OAuth)

Key Insight

Finding gaps in KRaft's verification is MORE valuable than proving correctness. A gap found in a widely-used system = instant credibility for Speckl.

# Prove Kafka — Project Plan Documented in `docs/PROVE-KAFKA-PLAN.md`. ## Summary **Don't replace Kafka. Prove it.** Specify Kafka's KRaft consensus protocol in SpeckDL, verify its safety invariants with Z3, and publish the findings. This is both the flagship demo for Speckl and the first consulting deliverable. ## Phases **Phase 0 — Compiler Foundation** - M0.1: TypeScript Reference Backend (Clean Build) - M0.2: Typed Intermediate Representation - M0.3: Z3 Verification Backend **Phase 1 — Kafka KRaft Specification** - M1.1: KRaft State Machine Specification - M1.2: KRaft Verification Results - M1.3: Producer Acks & Consumer Groups **Phase 2 — Rust Backend** - M2.1: Rust Code Generation - M2.2: KRaft Reference Implementation in Rust **Phase 3 — Publish & Market** - M3.1: Blog Post "We Formally Verified Kafka's Consensus" - M3.2: Show HN Launch - M3.3: Consulting One-Pager "Prove Your Distributed System" **Phase 4 — Expand the Proof Catalog** - M4.1: Raft Specification (etcd/Consul) - M4.2: TigerBeetle Ledger Deep Verification - M4.3: OAuth 2.0 / OIDC Flow Specification ## Dependency Graph ``` M0.1 → M0.2 → M0.3 → M1.1 → M1.2 → M1.3 ↓ ↓ M4.1 M3.1 → M3.2 M4.3 ↓ M3.3 M0.2 → M2.1 → M2.2 → M4.2 ``` ## Success Metrics - KRaft spec ≤ 300 lines of SpeckDL - ≥ 8 invariants verified - ≥ 1 gap/vulnerability found (gaps > proofs for credibility) - Z3 verification depth: 20 transitions - Rust within 2x of hand-optimized - Show HN ≥ 200 upvotes - ≥ 5 consulting inquiries - 4 proof catalog entries (KRaft, Raft, TigerBeetle, OAuth) ## Key Insight Finding gaps in KRaft's verification is MORE valuable than proving correctness. A gap found in a widely-used system = instant credibility for Speckl.

agent-cos commented

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

Author

Superseded by atomic issues #18–#32. Each milestone is now a one-shot agent ticket:

Phase 0: #18 (M0.1: TS bugs), #19 (M0.1: Delete WAT), #20 (M0.2: IR), #21 (M0.3: Z3)
Phase 1: #22 (M1.1: KRaft spec), #23 (M1.2: KRaft verify), #24 (M1.3: Producer/Consumer)
Phase 2: #25 (M2.1: Rust backend), #26 (M2.2: KRaft Rust reference)
Phase 3: #27 (M3.1: Blog), #28 (M3.2: Show HN), #29 (M3.3: Consulting one-pager)
Phase 4: #30 (M4.1: Raft), #31 (M4.2: TigerBeetle), #32 (M4.3: OAuth)

Closing this epic in favor of the atomic tickets.

Superseded by atomic issues #18–#32. Each milestone is now a one-shot agent ticket: **Phase 0:** #18 (M0.1: TS bugs), #19 (M0.1: Delete WAT), #20 (M0.2: IR), #21 (M0.3: Z3) **Phase 1:** #22 (M1.1: KRaft spec), #23 (M1.2: KRaft verify), #24 (M1.3: Producer/Consumer) **Phase 2:** #25 (M2.1: Rust backend), #26 (M2.2: KRaft Rust reference) **Phase 3:** #27 (M3.1: Blog), #28 (M3.2: Show HN), #29 (M3.3: Consulting one-pager) **Phase 4:** #30 (M4.1: Raft), #31 (M4.2: TigerBeetle), #32 (M4.3: OAuth) Closing this epic in favor of the atomic tickets.