From 7928c2b1da8099547b39ff02e15c505e0d0cf100 Mon Sep 17 00:00:00 2001 From: "Marcus (agent-cos)" Date: Sat, 9 May 2026 21:40:21 -0700 Subject: [PATCH] docs: Prove Kafka project plan (4 phases, 12 milestones, dependency graph only) --- docs/PROVE-KAFKA-PLAN.md | 313 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 313 insertions(+) create mode 100644 docs/PROVE-KAFKA-PLAN.md diff --git a/docs/PROVE-KAFKA-PLAN.md b/docs/PROVE-KAFKA-PLAN.md new file mode 100644 index 0000000..4fdf7bc --- /dev/null +++ b/docs/PROVE-KAFKA-PLAN.md @@ -0,0 +1,313 @@ +# Prove Kafka — Project Plan + +> *Don't replace Kafka. Prove it. Then prove everything else.* + +--- + +## Objective + +Specify Apache 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 in the "prove your distributed system" product line. + +--- + +## Guiding Principle + +Dependencies only. No wall-time estimates. Each milestone lists what must be true before it can start. + +--- + +## Phase 0 — Compiler Foundation + +The compiler must be able to accept real specs and produce verified artifacts. Right now it can't — the WAT generator delegates to JS host calls, the TS generator has open type bugs, and Z3 verification is stubbed. + +### M0.1 — TypeScript Reference Backend (Clean Build) + +**Target:** `speckl compile` produces idiomatic, runnable TypeScript from any `.speck` file. All 12 examples compile and pass generated tests. + +**Dependencies:** None (starts now) + +**Deliverables:** +- Fix engineering#9 (spurious `this.state` prefix in guards) +- Fix engineering#11 (record type emission for TS) +- Fix engineering#12 (5 expression pattern translations to JS) +- All 12 example specs compile to TypeScript without errors +- Generated TypeScript passes basic smoke tests (state transitions, guard checks, event emission) +- Delete WAT generator (superseded by IR→Rust→WASM path in M1.2) + +**Exit criteria:** `speckl compile examples/*.speck --target=typescript` produces `.ts` files that compile with `tsc --noEmit` and pass a generated test suite. + +--- + +### M0.2 — Typed Intermediate Representation + +**Target:** Compiler produces a typed IR between AST and backend generators. No generator duplicates type logic or parses raw AST. + +**Dependencies:** M0.1 complete + +**Deliverables:** +- Define IR schema: `SpeckIR` with typed state, actions, invariants, events, provenance annotations +- Refactor parser → `[AST] → type check → [SpeckIR]` pipeline +- All generators (TS, PROV-O, CycloneDX, SPDX) consume IR, not AST +- IR includes provenance annotations (source line → IR node mapping) + +**Exit criteria:** `speckl compile` produces IR as an intermediate artifact. Each generator consumes IR only. Provenance chain from source line to generated artifact is traceable. + +--- + +### M0.3 — Z3 Verification Backend + +**Target:** `speckl verify` compiles `invariant` and `verify` blocks to Z3 SMT-LIB assertions and reports satisfiability. + +**Dependencies:** M0.2 complete + +**Deliverables:** +- Z3 backend: translate `state` declarations to Z3 sort declarations, `init` to constraints, `action` guards to preconditions, `invariant` to assertion functions +- `speckl verify ` runs Z3 and reports: PASS (all invariants hold), FAIL (counterexample provided), UNKNOWN (timeout) +- Bounded model checking: verify invariants up to N state transitions (configurable depth) +- Counterexample generation: when an invariant fails, Z3 produces a concrete state trace showing the violation + +**Exit criteria:** `speckl verify examples/ToggleSwitch.speck` proves invariants hold. `speckl verify examples/Raft.speck --depth=5` runs bounded verification and reports results. + +--- + +## Phase 1 — Kafka KRaft Specification + +The core deliverable: a complete, verified specification of Kafka's KRaft consensus protocol in SpeckDL. + +### M1.1 — KRaft State Machine Specification + +**Target:** Kafka KRaft consensus protocol specified in SpeckDL. Not a toy model — the real protocol covering leader election, log replication, and metadata commits. + +**Dependencies:** M0.3 complete (need Z3 verification to validate the spec) + +**Deliverables:** +- `examples/KafkaKRaft.speck` — full KRaft spec including: + - State: term, votedFor, log entries, commitIndex, leaderId, cluster metadata + - Actions: RequestVote, AppendEntries, Commit, BecomeLeader, BecomeFollower + - Invariants: log matching, leader completeness, term monotonicity, no uncommitted data loss + - Events: LeaderElected, LogReplicated, Committed, TermChanged +- Each action has `require` guards matching KRaft's actual preconditions +- Invariants are the ones cited in the original Raft paper (Ongaro dissertation) and KRaft Kafka documentation + +**Exit criteria:** Spec compiles to TypeScript without errors. Z3 bounded verification runs without crashes. All invariants are stated and checkable. + +--- + +### M1.2 — KRaft Verification Results + +**Target:** Z3 verification of KRaft invariants, with documented findings. Gaps found are MORE valuable than invariants proven. + +**Dependencies:** M1.1 complete + +**Deliverables:** +- Run `speckl verify examples/KafkaKRaft.speck` at increasing depths (5, 10, 20 transitions) +- Document each invariant result: PASS (proven for depth N), FAIL (counterexample trace), UNKNOWN (timeout at depth N) +- For any FAIL results: document the counterexample, trace it to the KRaft implementation, determine if it's a spec gap or a real protocol vulnerability +- Written analysis: "What we proved, what we couldn't, and what we found" + +**Exit criteria:** Written verification report with concrete results for each KRaft invariant. At least one finding (gap or real vulnerability) documented with a counterexample trace. + +--- + +### M1.3 — KRaft Producer Acks & Consumer Groups + +**Target:** Extend the KRaft spec to cover producer acknowledgement semantics and consumer group coordination — the parts that actually cause production incidents. + +**Dependencies:** M1.2 complete + +**Deliverables:** +- `examples/KafkaProducer.speck` — producer ack levels (0=fire and forget, 1=leader ack, all=ISR ack), idempotent producer state, transaction coordinator +- `examples/KafkaConsumerGroup.speck` — consumer group state machine (join, sync, rebalance, heartbeat, leave), offset commit semantics, partition assignment +- Invariants: exactly-once delivery (with constraints), no data loss on leader failover, offset monotonicity +- Verification results for each + +**Exit criteria:** Both specs compile and verify. Producer ack invariant proves that `acks=all` prevents data loss on leader failure (bounded). Consumer group rebalance is modeled and verified for safety (no concurrent assignments to same partition). + +--- + +## Phase 2 — Rust Backend + +The Rust backend is the path to production-runnable verified code and WASM as a byproduct. + +### M2.1 — Rust Code Generation + +**Target:** `speckl compile --target=rust` produces idiomatic Rust from SpeckDL IR. + +**Dependencies:** M0.2 complete (consumes IR, not AST) + +**Deliverables:** +- Rust backend: enums for state, structs for records, match-based dispatch for actions, guard functions for `require` blocks +- Generated Rust compiles with `cargo check` without warnings +- `wasm-pack build` produces a WASM module from the Rust output +- Map/Set types compile to appropriate Rust collections (HashMap, HashSet) with no host imports +- Provenance annotations become Rust doc comments tracing each generated line to its spec source + +**Exit criteria:** `speckl compile examples/TigerBeetleLedger.speck --target=rust` produces Rust that compiles and passes basic state machine tests. `wasm-pack build` on the output produces a valid `.wasm` module. + +--- + +### M2.2 — KRaft Reference Implementation in Rust + +**Target:** Compile `KafkaKRaft.speck` to Rust, run the generated code, demonstrate it matches the spec's invariants at runtime. + +**Dependencies:** M1.1 complete (need the spec), M2.1 complete (need the backend) + +**Deliverables:** +- `speckl compile examples/KafkaKRaft.speck --target=rust` produces a runnable Rust module +- Runtime guard checks fire and prevent invariant violations +- Provenance trace: each Rust function has a doc comment pointing to the source `.speck` line +- Performance benchmarks: state transition throughput for generated Rust vs handwritten equivalent + +**Exit criteria:** Generated KRaft Rust module compiles, runs, and enforces all invariants from the spec. Benchmark shows generated code within 2x of hand-optimized Rust for state transitions. + +--- + +## Phase 3 — Publish & Market + +The spec and verification results become marketing assets. + +### M3.1 — Blog Post: "We Formally Verified Kafka's Consensus" + +**Target:** Long-form technical blog post documenting the KRaft specification and verification findings. + +**Dependencies:** M1.2 complete (need results), M0.3 complete (need Z3 to explain) + +**Deliverables:** +- Blog post on speckl.scoble.me (or scott.scoble.me if higher traffic) +- Structure: Problem → Method → Spec overview → Verification results → Findings → Implications +- Include the full `.speck` file inline (it's the hero artifact) +- If a real gap/vulnerability was found in M1.2, lead with that +- Cross-post to Hacker News, Reddit r/distributed_systems, Lobsters + +**Exit criteria:** Published blog post with working code examples. HN submission ready. + +--- + +### M3.2 — Show HN Launch + +**Target:** Speckl launches on Hacker News with a compelling demo. + +**Dependencies:** M0.3 complete (Z3 verification works), M1.2 complete (KRaft results), M3.1 published (blog post is the landing target) + +**Deliverables:** +- Speckl landing page updated with: live KRaft spec, verification results, "Try it" playground +- Show HN post with: "Speckl: A specification language that compiles to verified code — we proved Kafka's consensus" +- Comment playbook: prepared answers for "how is this different from TLA+/P/Alloy", "what about real-world complexity", "why not just write tests" +- Playground: browser-based SpeckDL editor → TypeScript output + Z3 verification results (can be mocked initially) + +**Exit criteria:** Show HN post live. Landing page live. Playground functional enough for visitors to type a spec and see output. + +--- + +### M3.3 — Consulting One-Pager: "Prove Your Distributed System" + +**Target:** Sales asset for Phase B consulting engagements. + +**Dependencies:** M1.2 complete (KRaft results are the proof case), M3.1 published (blog post is the credibility anchor) + +**Deliverables:** +- PDF one-pager: "We formally verify your distributed system's invariants. Here's what we proved about Kafka." +- Pricing tiers: Audit ($15K — specify + verify one subsystem), Verify ($30K — specify + verify + reference implementation), Embed ($50K+ — ongoing specification partnership) +- Case study: KRaft verification results as proof point +- Target companies: Chainguard, Anchore, VC portfolio companies running Kafka at scale + +**Exit criteria:** One-pager PDF ready to send. Blog post is live and linkable. + +--- + +## Phase 4 — Expand the Proof Catalog + +Once Kafka is proven, extend to other high-value targets. + +### M4.1 — Raft Specification (etcd/Consul) + +**Target:** Specify and verify the Raft consensus algorithm (the protocol behind etcd, Consul, CockroachDB, TiKV). + +**Dependencies:** M1.2 complete (proven methodology), M0.3 complete (Z3 verification) + +**Deliverables:** +- `examples/Raft.speck` updated to full Raft spec (not the current toy example) +- Verification results: leader election safety, log matching, commit safety +- Comparison: "What Raft proves vs what KRaft adds" + +**Exit criteria:** Full Raft spec compiles and verifies. Written analysis comparing Raft vs KRaft verification results. + +--- + +### M4.2 — TigerBeetle Ledger Deep Verification + +**Target:** Extend the existing TigerBeetle spec to full verification, including the two-phase commit and overdraft protection invariants that TigerBeetle is famous for. + +**Dependencies:** M0.3 complete, M2.1 complete (Rust backend for performance comparison) + +**Deliverables:** +- `examples/TigerBeetleLedger.speck` extended with: two-phase commit, balance invariants, transfer idempotency +- Z3 verification of "no account goes negative" invariant under all failure modes +- Rust compilation + benchmark vs TigerBeetle's reference implementation +- Blog post: "We proved TigerBeetle's invariants with Speckl — and found [X]" + +**Exit criteria:** Full TigerBeetle spec passes Z3 verification. Performance comparison documented. Blog post drafted. + +--- + +### M4.3 — OAuth 2.0 / OIDC Flow Specification + +**Target:** Specify the OAuth 2.0 authorization code flow (including PKCE) as a state machine and verify its invariants. + +**Dependencies:** M0.3 complete + +**Deliverables:** +- `examples/OAuth2AuthorizationCode.speck` — full auth code flow with PKCE +- Invariants: no token leakage, CSRF protection, code reuse prevention, replay attack resistance +- Verification: prove that PKCE prevents authorization code interception +- Sales angle: "We proved OAuth works. Can we prove YOUR auth works?" + +**Exit criteria:** OAuth spec compiles and verifies. At least one PKCE invariant proven. Marketing-ready asset. + +--- + +## Dependency Graph + +``` +M0.1 (TS Backend Clean) + └──→ M0.2 (Typed IR) + └──→ M0.3 (Z3 Backend) + ├──→ M1.1 (KRaft Spec) + │ └──→ M1.2 (KRaft Verification) + │ ├──→ M1.3 (Producer/Consumer) + │ └──→ M3.1 (Blog Post) + │ ├──→ M3.2 (Show HN) + │ └──→ M3.3 (Consulting One-Pager) + ├──→ M4.1 (Raft) + └──→ M4.3 (OAuth 2.0) + +M0.2 ──→ M2.1 (Rust Backend) + └──→ M2.2 (KRaft Rust Reference) + └──→ M4.2 (TigerBeetle Deep) + +M1.2 ──→ M4.1, M4.2, M4.3 +``` + +--- + +## Success Metrics + +| Metric | Target | +|--------|--------| +| KRaft spec lines | ≤ 300 lines of SpeckDL | +| Invariants verified | ≥ 8 (leader election, log matching, commit safety, etc.) | +| Gaps/vulnerabilities found | ≥ 1 (a gap is worth more than a proof) | +| Z3 verification depth | 20 transitions for core invariants | +| Rust backend performance | Within 2x of hand-optimized for state transitions | +| Show HN upvotes | ≥ 200 | +| Consulting inquiries from blog | ≥ 5 | +| Proof catalog entries | 4 (KRaft, Raft, TigerBeetle, OAuth) | + +--- + +## Open Items + +- **Z3 depth vs. completeness:** Bounded model checking at depth 20 is not exhaustive. Need a strategy for "verified up to N transitions" vs. "verified for all transitions." Document this honestly. +- **KRaft spec scope:** Kafka's KRaft is ~15K lines of Java. The SpeckDL spec must cover the consensus core, not the full broker. Need a clear scope boundary. +- **Show HN timing:** Coordinate with M3.1 publication. Don't launch the HN post until the blog post and playground are live. +- **Consulting pricing:** The one-pager has draft tiers ($15K/$30K/$50K+). Scott needs to review and approve before any outreach. \ No newline at end of file