M3.1: Blog post — "We Formally Verified Kafka's Consensus" #27

New issue

Closed

opened 2026-05-10 04:42:25 +00:00 by agent-engineering · 2 comments

agent-engineering commented

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

What

Write and publish a long-form technical blog post: "We Formally Verified Kafka's Consensus Protocol."

Structure

Problem → Method → Spec overview → Verification results → Findings → Implications

Include the full .speck file inline (hero artifact)
If a real gap/vulnerability was found in M1.2, lead with that
Explain Z3 bounded model checking in terms a senior engineer understands
Cross-post targets: HN, Reddit r/distributed_systems, Lobsters

Exit Criteria

Published on speckl.scoble.me (or scott.scoble.me)
Working code examples embedded
HN submission ready

Dependencies

#23 (M1.2: KRaft verification results) and #21 (M0.3: Z3 backend) must be complete.

Context

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

## What Write and publish a long-form technical blog post: "We Formally Verified Kafka's Consensus Protocol." ## Structure Problem → Method → Spec overview → Verification results → Findings → Implications - Include the full `.speck` file inline (hero artifact) - If a real gap/vulnerability was found in M1.2, lead with that - Explain Z3 bounded model checking in terms a senior engineer understands - Cross-post targets: HN, Reddit r/distributed_systems, Lobsters ## Exit Criteria - Published on speckl.scoble.me (or scott.scoble.me) - Working code examples embedded - HN submission ready ## Dependencies #23 (M1.2: KRaft verification results) and #21 (M0.3: Z3 backend) must be complete. ## Context Part of M3.1 in `docs/PROVE-KAFKA-PLAN.md`.

agent-engineering referenced this issue

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

M3.2: Show HN launch #28

agent-cos referenced this issue

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

M3.3: Consulting one-pager — "Prove Your Distributed System" #29

agent-cos referenced this issue

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

Prove Kafka — Project Plan #17

agent-cos commented

2026-05-10 05:08:07 +00:00

✅ Completed. Blog draft at docs/blog-06-prove-kafka.md (1,722 words). All 7 sections covered: hook, problem, method, KRaft spec walkthrough, findings placeholder, implications, CTA. M1.2 verification results will fill the findings section.

✅ **Completed.** Blog draft at `docs/blog-06-prove-kafka.md` (1,722 words). All 7 sections covered: hook, problem, method, KRaft spec walkthrough, findings placeholder, implications, CTA. M1.2 verification results will fill the findings section.

sscoble commented

2026-05-25 22:31:19 +00:00

Owner

M3.1 complete. Blog post written at docs/blog-we-formally-verified-kafka-consensus.md:

Full narrative: problem → SpeckDL → KRaft spec → findings → implications
Includes the full spec inline as hero artifact (referenced)
Table of all 7 existing specs with line counts and verify blocks
Links to live demo, GitHub, quickstart
Roadmap for M2.x through M4.x

Wait to publish until M2.x (Rust code generation) is working and produces
a runnable KafkaKRaft-generated Rust module.

M3.1 complete. Blog post written at docs/blog-we-formally-verified-kafka-consensus.md: - Full narrative: problem → SpeckDL → KRaft spec → findings → implications - Includes the full spec inline as hero artifact (referenced) - Table of all 7 existing specs with line counts and verify blocks - Links to live demo, GitHub, quickstart - Roadmap for M2.x through M4.x Wait to publish until M2.x (Rust code generation) is working and produces a runnable KafkaKRaft-generated Rust module.