Show HN: Formally Verified Leaderless Log Protocol for Kafka

5 points by sijieg 3 months ago · 1 comment · 1 min read

We open-sourced the TLA+ and Fizzbee verified spec behind Ursa's storage engine. Verification across ~200K states caught a design bug that years of production missed. We then handed the spec to Claude Code — it produced a working Rust implementation (concurrent producers, compaction, fencing) without back-and-forth. We think verified specs are the best harness for coding agents: open-source the spec, let anyone implement it.