diff --git a/docs/PROVE-KAFKA-PLAN.md b/docs/PROVE-KAFKA-PLAN.md index 4fdf7bc..00bb9b7 100644 --- a/docs/PROVE-KAFKA-PLAN.md +++ b/docs/PROVE-KAFKA-PLAN.md @@ -305,6 +305,30 @@ M1.2 ──→ M4.1, M4.2, M4.3 --- +## Issue Tracking + +Each milestone has an atomic Forgejo issue (one-shot, agent-friendly): + +| Milestone | Issue | +|-----------|-------| +| M0.1: TS bugs | #18 | +| M0.1: Delete WAT | #19 | +| M0.2: Typed IR | #20 | +| M0.3: Z3 backend | #21 | +| M1.1: KRaft spec | #22 | +| M1.2: KRaft verify | #23 | +| M1.3: Producer/Consumer | #24 | +| M2.1: Rust backend | #25 | +| M2.2: KRaft Rust ref | #26 | +| M3.1: Blog post | #27 | +| M3.2: Show HN | #28 | +| M3.3: Consulting PDF | #29 | +| M4.1: Raft spec | #30 | +| M4.2: TigerBeetle | #31 | +| M4.3: OAuth 2.0 | #32 | + +Epic #17 closed — superseded by #18–#32. + ## 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.