Temporal collisions in at-least-once message brokers — formal verification with TLA+ templates
17 views
Skip to first unread message
Illia Rochev
Jul 14, 2026, 4:11:38 PM (2 days ago) Jul 14
to tlaplus
Hi everyone,
I'd like to share a project I've been working on that uses TLA+ to detect a specific class of bugs in distributed message brokers.
The problem: In systems with at-least-once delivery (Kafka, RabbitMQ, NATS JetStream, Pulsar), there's a temporal collision window between storing a result and committing the offset/ack. If a consumer crashes in this window, the message is redelivered and the result is executed twice. This is well-known in practice but rarely formalized.
The approach: I built a toolchain that generates TLA+ specifications from parameterized YAML configurations. The key insight is that the crash window follows a repeatable pattern across brokers — the protocol is the same, only the variable names change. So instead of writing TLA+ from scratch for each broker, I use templates with placeholders:
- Kafka: offset, topic, partition → Process, StoreResult, CommitOffset
- NATS: stream, seqno → Process, StoreResult, SendAck
- RabbitMQ: taskState, deliveryTag → Process, StoreResult, AckMessage
- Pulsar: batchId, cursor → Process, StoreResult, CommitCursor
Each template models 4 modes: faulty (crash window), idempotent (dedup guard), two-phase async (split commit), and firefly (pulse-coupled sync).
Results: 16 templates verified by TLC, ~14k total states explored in ~14s. One negative finding: pulse-coupled synchronization (firefly mode) does NOT eliminate the crash window — the gap between StoreResult and CommitOffset exists regardless of commit timing.
I also built chaos cross-validation: Docker fault injection confirms TLC's predictions by injecting the exact crash timing the model predicts.
I'd like to share a project I've been working on that uses TLA+ to detect a specific class of bugs in distributed message brokers.
The problem: In systems with at-least-once delivery (Kafka, RabbitMQ, NATS JetStream, Pulsar), there's a temporal collision window between storing a result and committing the offset/ack. If a consumer crashes in this window, the message is redelivered and the result is executed twice. This is well-known in practice but rarely formalized.
The approach: I built a toolchain that generates TLA+ specifications from parameterized YAML configurations. The key insight is that the crash window follows a repeatable pattern across brokers — the protocol is the same, only the variable names change. So instead of writing TLA+ from scratch for each broker, I use templates with placeholders:
- Kafka: offset, topic, partition → Process, StoreResult, CommitOffset
- NATS: stream, seqno → Process, StoreResult, SendAck
- RabbitMQ: taskState, deliveryTag → Process, StoreResult, AckMessage
- Pulsar: batchId, cursor → Process, StoreResult, CommitCursor
Each template models 4 modes: faulty (crash window), idempotent (dedup guard), two-phase async (split commit), and firefly (pulse-coupled sync).
Results: 16 templates verified by TLC, ~14k total states explored in ~14s. One negative finding: pulse-coupled synchronization (firefly mode) does NOT eliminate the crash window — the gap between StoreResult and CommitOffset exists regardless of commit timing.
I also built chaos cross-validation: Docker fault injection confirms TLC's predictions by injecting the exact crash timing the model predicts.
Code: Currently private, but I'm preparing it for release.
I haven't seen this specific pattern (temporal collisions in at-least-once brokers) discussed on this list. Has anyone here formalized similar consumer offset timing issues? I'd be curious to hear how others model the commit window.
Reply all
Reply to author
Forward
0 new messages