Formal proof of ACK temporal collision (at-least-once delivery double execution) with TLA+ and chaos cross-validation

[illyar80]

Summary

We independently proved and reproduced the ACK temporal collision in RabbitMQ — a race condition where a consumer crashes after storing a result but before the AMQP acknowledgment reaches the broker, causing the redelivered message to be processed twice.

This is documented behavior (RabbitMQ at-least-once delivery guarantees), not an implementation bug. Our contribution is:

1. Formal proof via TLA+ model checking — exhaustively explores all interleavings
2. Chaos cross-validation via Toxiproxy — confirms the mathematical prediction in a physical network
3. Cross-broker reproduction — identical scenario reproduced on NATS JetStream, proving it is a fundamental distributed systems problem

---

The Scenario

Consumer                 RabbitMQ                  DB
   |                        |                      |
   |  consume(msg)          |                      |
   |<-----------------------|                      |
   |  process(msg)          |                      |
   |  store_result(msg)     |                      |
   |---------------------------------------------->|
   |                        |                      |
   |  *** CRASH ***         |                      |
   |  (ACK not sent)        |                      |
   |                        |                      |
   |                        |  redeliver(msg)      |
   |<-----------------------|                      |
   |  process(msg) AGAIN    |                      |
   |  store_result(msg)     |       *** DOUBLE *** |
   |---------------------------------------------->|

Formal Proof (TLA+)

We modeled the system as a TLA+ specification with three actions:

• DeliverTask — broker sends a message to consumer
• ExecuteTask — consumer stores result in DB
• Disconnect — network failure before ACK
• RedeliverUnacked — broker re-dispatches the unacknowledged message

Results:

• Faulty model: 108 states, depth 7 — invariant InvariantNoDoubleExecution violated
• Idempotent model (with should_skip() guard): 277 states, depth 11 — PASS (no counterexamples anywhere)

Chaos Cross-Validation

We wrote a pilot (pilot_rabbitmq/) that:

1. Starts RabbitMQ, PostgreSQL, Toxiproxy, and a Python consumer via Docker Compose
2. Publishes a task message
3. Waits 1s (the consumer stores the result)
4. Disables the Toxiproxy RabbitMQ proxy (simulates AMQP connection drop)
5. Waits 8s (past the consumer heartbeat timeout)
6. Re-enables the proxy, waits 5s for redelivery
7. Counts DB rows

Results:

• Faulty consumer: 2 DB rows — confirmed double execution
• Idempotent consumer (with should_skip() check): 1 DB row — single execution

Cross-Broker Validation

We adapted the same TLA+ model and chaos pilot for NATS JetStream. The results matched:

Broker	Mode	TLC States	TLC Depth	TLC Result	Chaos Result
RabbitMQ	Faulty	108	7	VIOLATED	2 executions
RabbitMQ	Idempotent	277	11	PASS	1 execution
NATS JetStream	Faulty	47	6	VIOLATED	2 executions
NATS JetStream	Idempotent	105	9	PASS	1 execution

Verdict: 4/4 TLC predictions matched 4/4 chaos experiments.

The Fix

The recommended consumer-side fix is the idempotent consumer pattern:

def callback(ch, method, properties, body):
    task_id = int(body.decode())
    
    # Idempotent guard: check before processing
    if should_skip(task_id):
        ch.basic_ack(delivery_tag=method.delivery_tag)
        return
    
    store_result(task_id)  # INSERT into DB
    ch.basic_ack(delivery_tag=method.delivery_tag)

The TLA+ model proved this fix under all possible failure interleavings — not just happy-path testing.

Repository

All code is open-source at https://github.com/illyar80/utlp-lpm-agent:

• pilot_rabbitmq/ — RabbitMQ pilot (TLA+ specs, consumer, Docker Compose, pilot script)
• pilot_nats/ — NATS JetStream pilot (same structure)
• beyond_ai_coders.md — full writeup

Discussion

We believe this is valuable as a formally verified demonstration of RabbitMQ's at-least-once delivery semantics and the critical importance of the idempotent consumer pattern. Our TLA+ model and chaos framework are portable to any message broker — we proved this by running the identical experiment on NATS JetStream.

We would love feedback from the RabbitMQ team and community:

• Do you see value in including formal TLA+ specs in the RabbitMQ documentation as reference?
• Are there any RabbitMQ-specific mitigation strategies (beyond consumer idempotence) that could address this at the broker level?

[michaelklishin]

No kidding, consumers may get redeliveries and may need to be idempotent. Our tutorial 2 says as much.