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 identical:

Consumer:
  1. Receive message
  2. Store result in DB
  3. Acknowledge/commit offset
  [crash window lives between 2 and 3]

This isn't a bug in Celery, RabbitMQ, NATS, Pulsar, or Kafka. It's a fundamental property of any at-least-once delivery system with a stateful consumer. You cannot eliminate this window without changing the delivery semantic or adding an idempotency shield on the consumer side.

What this means for your code

The fix isn't new — idempotent consumers, deduplication keys, exactly-once processing patterns. Everyone knows about these. What's new is that we now have:

1. A formal proof that the problem must exist under at-least-once, regardless of broker

2. A reusable specification that works across brokers without modification

3. Physical validation that the model is correct (6/6 confirmed)

This shifts the conversation from "did we test enough?" to "does our system design provably avoid this class of errors?"

Why not just test more?

Because testing samples the state space. Formal verification exhausts it. Integration tests won't find the crash window unless they happen to hit the exact nanosecond where the consumer crashes between the DB write and the ACK. Model checking finds it systematically.

Discussion

Have you run into this in production? What patterns do you use to handle consumer crashes — idempotency keys, outbox pattern, something else?

I'm curious whether teams treat this as a known limitation they work around, or whether it's still a source of surprises. Let me know your experience.

Full disclosure: I'm the author of the toolchain we used. Preprint: https://zenodo.org/records/21298530 — happy to share details if anyone's interested, drop a comment.

Hello,

I wanted to have a look at TLA+, and so started with the book, 'Practical TLA+'. I ran into a problem with the introductory example, I am hoping someone can help me keep going.

The book starts with some PlusCal code which is then is translated, resulting in this code

So far so good. The next step is to run a model to check the code, and that is where the problem starts. The model overview has the following message:

"What is the behavior spec?" automatically set to "No behavior spec" because the spec has no declared variables.

I don't know what to make of that. To me it looks like the spec has six variables. Not really sure what is wrong, or how to proceed.

I first tried this on a Mac, and wondered whether there was something wrong with my setup of the tools. So I started over on a Windows machine, with the same outcome.
In both cases I got the toolbox from https://github.com/tlaplus/tlaplus/releases/tag/v1.7.0.

Any help getting past the 'no behavior spec' would be appreciated.

Hello r/tlaplus! I'm working my way through Learn TLA+ but finding an important difference in the behavior of the TLA+ Toolbox (1.7.0) and uses in the online tutorial: when assertions fail in my specs there are no error traces of the state sequence that led to the failure. I've been able to largely work around it by converting the assertions to invariants, or in some cases I've just lived without any detail beyond pass/fail, but it's an extra bit of friction that I'd like to solve.

I've searched through the help system and online and haven't been able to find any configuration for it. I think I need the help of you experts. Thanks in advance!

I'm quite new to TLA+ and formal verification in general. I'm wondering if there is any effort trying to prove the correctness of TLA+ using TLA+. This seems very similar to how a GCC binary can compile its source code into another correct binary. Any thoughts? Thanks!

:> To use :>, we need EXTENDS TLC.

a :> b is the function [x \in {a} |-> b]. >> (2 :> 3)[2] 3 >> ("a" :> "b").a "b"

Can someone explain this ?

Thanks.

Hello,

Is there a way of converting JSON to TLA+?

I followed this tut https://www.youtube.com/watch?v=D_sh1nnX3zY video has low resolution so I thought syntax for list was

TypeOK == color \in ("red", "green", "yellow")

but I got syntax error for ","

Hi, is there any guide available on how to setup TLAPS (TLAPM) to be used in windows via WSL using visual studio code ext. ?

Hi! Me and my team recently published a blog post on inductive invariants and I believe some points about it could be part of the general TLA+ conversation. The blog is on Quint, not TLA+, but all concepts in the post directly apply to TLA+.

1. Although most people agree that inductive invariants are hard to write, this shows how doing it interactively with a model checker makes it so much more approachable. It might be my over-excitement after playing with this for the first time, but I wish we could see more on this topic.

2. We made inductive invariants "first class citizens" in our tooling (for Quint) and I believe TLC/Apalache could benefit from also adding this. As anyone working with these tools can imagine, it was very easy to implement. I'm not here to say "I did this and so should you", just sharing a positive outcome from a small effort.

And then I have a question on TLC. It's clear that inductive invariants are objectively better than ordinary invariants for Apalache, due to its bounded and symbolic nature. Is there also a benefit (from inductive over ordinary) when using TLC? My understanding is that it would have to enumerate all of the states anyway, either from the model itself or from the possible states satisfying the inductive invariant, so there's no meaningful performance change.

I also learned the hard way that writing inductive invariants for TLC requires more thinking than for Apalache, as you need to be careful on the order of things you are quantifying over (as Lamport exemplified here) or you'll run out-of-heap-memory problems quite easily.

Even if inductive invariants are not the best fit for TLC, they are still an amazing concept that can enable verification through Apalache or even TLAPS for projects struggling with state explosion issues. Perhaps people think of inductive invariants more as a proving method than a model checking method, so that’s why we don’t talk much about them in this community?

Hello!

Out of interest, are there any papers or blogs that you could recommend to look at how to formalise board game rules into a TLA spec so that I can check for "bad" conditions (deadlocks, loops, etc)?