Show HN: Formally Verified Leaderless Log Protocol for Kafka

Category: database

Tags: distributed-systems, formal-verification, protocol-design, tla-plus, stream-processing

Score: 8.3/10 (Innovation: 8, Technical: 9, Documentation: 9, Utility: 7)

This project provides a formally verified, leaderless distributed append-only log protocol designed as a drop-in replacement for Kafka's consensus layer. It's interesting because it introduces the 'coordination-delegated' pattern, separating consensus logic into an external linearizable store to enable stateless, concurrent writers, and its specification has been used in a production system (Ursa).

Target audience: backend devs, data engineers, devops, distributed systems researchers

Repository: https://github.com/lakestream-io/leaderless-log-protocol · TLA · NOASSERTION

View on Hacker News