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

You know the story. You write a consumer, test it locally, deploy to staging, everything green. Then in production, the same message gets processed twice. Orders are duplicated. Notifications go out twice. Everyone blames "a race condition" and moves on. We spent the last few months formally verifying what actually happens when consumers crash with at-least-once delivery semantics. The short version: it doesn't matter which broker you use . The race condition is a property of the delivery contract, not a bug in the implementation. What we did Instead of writing more integration tests hoping to reproduce the timing, we wrote a formal specification of the consumer-broker interaction in TLA+ (the specification language by Leslie Lamport). The model checker exhaustively explores every possible interleaving of events — not just the ones you think to test. Then we took the counterexamples from the model and validated them in real running systems using Docker + Toxiproxy (network fault injection). If the math said "double-execution is possible", we confirmed it with actual containers. What we found We applied this pipeline to five different systems: Celery — ACK timeout + network blip: the model found the crash window at depth 9 (444 states). Chaos confirmed it: task executed twice. RabbitMQ — consumer stores result, drops connection before AMQP ACK. Same pattern. 108 states, depth 7. Chaos confirmed. NATS JetStream — consumer crashes after DB write, before ACK. 47 states, depth 6. Docker kill + Toxiproxy confirmed: duplicate execution. Apache Pulsar — batch consumer crashes between Process and SendAck. 21 states, depth 4. Chaos confirmed: 2 DB rows for 1 message. Kafka — consumer commits offset after processing. Crash between StoreResult and commitSync(). Same result: double execution. Every single time, the model predicted the collision and chaos confirmed it. The insight The spec is the same across all five systems. The variable names change, but the topology is identic