Your integration tests pass, but your message queue still double-processes in production

Illia Rochev — Sun, 12 Jul 2026 20:32:42 +0000

You write a consumer, test it locally, everything green. Deploy to staging — green. Then in production, the same message gets processed twice. Orders are duplicated. Notifications fire twice. The team blames "a race condition" and moves on.

This isn't a bug in your broker. It's a structural property of at-least-once delivery. And it's provable.

Who needs to care? If you write Kafka consumers in production — a backend engineer debugging duplicate orders, a platform team standardizing on at-least-once delivery, or an architect choosing between idempotency, transactional outbox, and exactly-once patterns — this problem affects your system whether or not you've seen evidence of it yet. Integration tests won't find it because they sample the state space. Documentation tells you to make consumers idempotent but does not explain why the crash window is structurally unavoidable, or which mitigations actually hold up under formal analysis. This article gives the formal answer.

The crash window

Every at-least-once broker has the same topology:

Consumer:
  1. Receive message
  2. Store result in database
  3. Acknowledge / commit offset

The crash window lives between steps 2 and 3. If the consumer crashes after writing the result but before acknowledging, the broker redelivers. The result is stored twice. Five different brokers — same topology, same crash window.

This is not a testing gap. Integration tests sample the state space. An interleaving where the crash lands in exactly that window may take millions of runs to hit — or may never hit in staging because production traffic shapes timing differently. Absence of evidence is not evidence of absence.

What formal verification adds

We built a verification pipeline that replaces sampling with exhaustion. The approach is:

Model the system — a formal specification of the consumer-broker interaction with explicit states for store, crash, redeliver, and commit
Check exhaustively — the model checker explores every possible interleaving of events, not just the ones that happen to occur during testing
Validate physically — predicted collisions are reproduced with real Docker containers and network fault injection (Toxiproxy)

The pipeline covers three brokers (Kafka, RabbitMQ, NATS JetStream) across four delivery modes — 108 unique configurations in total. Every configuration is checked exhaustively, not sampled.

Industry adoption confirms the same finding

Our results are not an academic curiosity. Llingr, a Kafka consumer engine with formal verification at its core, independently discovered the same class of bug during TLA+ model checking of their offset commit protocol. They found a race between CommitTick and partition revocation — a direct variant of the crash window — where an offset could be committed during a revoked window, producing silent duplicate processing. Their verification covered over 1.1 billion distinct states and 4.5 billion transitions across 25 verified properties.

This is production infrastructure discovering the same structural collision. The problem is real, it's systematic, and it's broker-independent.

What the numbers show

Across 108 configurations, the temporal collision is structurally invariant.

Mode	Verdict	What it means
Faulty	Collision (all 27 configs)	Crash after store before ACK always produces double execution
Idempotent	Pass (18/27 configs)	A `should_skip()` guard prevents redelivery — but only if correctly implemented
2async	Collision (18/27 configs)	Async store + commit widens the window, doesn't close it
Firefly	Collision (54/81 configs)	Pulse-coupled sync does NOT eliminate the crash window

The firefly result deserves emphasis. Pulse-coupled synchronization (two consumers phase-locking before committing) is a known technique from biological oscillators — fireflies synchronizing their flashes. Applied to Kafka consumers, it fails. The crash window exists within a single consumer's lifecycle: store → crash → redeliver. No amount of phase alignment between consumers can protect an individual consumer's internal store-then-commit sequence. Synchronization governs timing, not atomicity.

Idempotent consumers (checking should_skip() before execution) are the only reliable mitigation. There is no architectural trick around this — the crash window is a topological consequence of the at-least-once delivery contract.

LLMs are not the answer (yet)

We tested a GPT-4o-mini predictor on the same 108 configurations (540 calls, temperature 0.7). The result: recall 94.4%, specificity 1.1%, balanced accuracy 47.8% — below random chance. The model defaulted to "yes" 96% of the time. A trivial "always yes" baseline performs identically.

The role of LLMs in this domain is specification generation, not standalone detection. A formally verified spec checked by an exhaustive model checker is reliable. An LLM judge is not.

The practical takeaway

If you run at-least-once consumers:

Assume every message can be delivered twice — because structurally, it can. This is not pessimism, it's a provable property of the delivery contract.
Idempotency is not optional — a should_skip() guard, deduplication key, or exactly-once processing pattern is the only reliable defense.
Integration tests cannot prove absence — they sample the state space. Formal verification exhausts it. If your architecture must never double-execute (payments, idempotency keys, inventory), model checking is the appropriate tool.

The crash window is not a bug. It's a law of distributed systems — like the CAP theorem or the FLP result. You can't fix it. You can only design around it.

Full methodology and detailed results are available as a preprint (DOI: 10.5281/zenodo.21298530). The toolchain is not publicly available at this time.