sscoble/speckl
1
0
Fork 0
Code Issues 2 Pull requests Projects Releases Packages Wiki Activity Actions
speckl/docs/PROVE-KAFKA-PLAN.md

14 KiB
Raw Blame History

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 <file> 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.