Temporal collisions in at-least-once message brokers — formal verification with TLA+ templates
Illia Rochev
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.
Neil Talap
To verify events in a bus, you cannot only verify the events themselves; you now have to verify every single service, or at least faithfully model every component, that connects to the bus if those components affect the invariant you're trying to prove.
And as a result, you don't get a verified implementation; you can never state the implementation has been verified. It has only been modeled. Lamport designed TLA+ for this exact purpose, for people to first think about the system and invariants before writing any code.
To ask: What is the system? What are its states? What must always remain true?
Illia Rochev
Hi Neil,
Thank you for the sharp critique — these are important points worth addressing.
On “horribly designed systems”: I agree. The prevalence of temporal collision bugs in production systems (documented across all four brokers) is itself evidence that the bus decoupling pattern is widely misapplied. Our paper explicitly calls this out: the fix is not better idempotency guards but better system design where the consumer’s processing is within the transaction boundary.
On “you must verify every service”: Correct, and our models do exactly this. The TLA+ specifications model the full protocol — not just the broker, but the consumer’s store-before-commit path as well. The invariant execCount ≤ 1spans both the consumer and broker state machines. That said, our models necessarily abstract away everything outside this protocol boundary, which is a deliberate scope choice, not a claim of completeness.
On “the protocol is the same, only variable names change”: This is the strongest critique and fair. What I should have said more precisely: the protocol pattern — process → store → crash-before-commit → redeliver → duplicate execution — is structurally identical across brokers because it follows from the at-least-once delivery contract itself, not from any broker-specific implementation detail. The variable names change (offset vs. seqno vs. deliveryTag), but the state machine shape (Ready → Processing → Stored → Crashed → Redelivered) and the crash window between Store and Commit are the same. Whether this constitutes an “invariant” in the TLA+ sense is debatable — it’s more accurately a structural property of the protocol class. Our paper formalizes each broker independently and then observes the structural isomorphism, rather than assuming it a priori.
On TLA+ for thinking vs. verification: I think you and Lamport would agree that our approach aligns with his intent — we use TLA+ to first prove the collision exists structurally (via exhaustive state-space exploration), then cross-validate with physical fault injection. The 16 templates are not “verified implementations”; they are formal arguments that a specific property holds (or fails to hold) under all possible interleavings. The chaos experiments then confirm the model’s predictions match physical reality. This two-layer approach — deductive proof plus empirical confirmation — is closer to how formal methods should be applied in practice.