[tlaplus] Re: Temporal collisions in at-least-once message brokers — formal verification with TLA+ templates

[Neil Talap <khairtalap@xxxxxxxxx>]

The broker is too often used in horribly designed systems. I don't think it's an overstatement to simply call almost all, if not all, systems that use bus decoupling incorrectly designed. People lean on them too hard for the decoupling they think to be scalable. Yet they never design for the correct invariants. It irritates me, to say the least, when reading about it.

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.

This assumption is too strong: "the protocol is the same, only the variable names change"; this itself is not an invariant.

If your goal is to verify systems, TLA+ has never been designed to do that; it might do that to an extent, but it was designed to force engineers to think first.
To ask: What is the system? What are its states? What must always remain true?

Only after answering those questions should code exist.

On the end note, I must say, I believe buses have a place and time for their use. But I also believe virtually all implementations are incorrect and were utilized as a result of a dogma. I also believe these very same people never use them correctly. The bar for good engineering has fallen even lower in recent years.

On Wednesday, July 15, 2026 at 1:11:38 AM UTC+5 Illia Rochev wrote:

Hi everyone,

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.

Code: Currently private, but I'm preparing it for release.

https://www.linkedin.com/pulse/beyond-ai-coders-why-future-distributed-systems-proven-илья-рочев-cftef/

I haven't seen this specific pattern (temporal collisions in at-least-once brokers) discussed on this list. Has anyone here formalized similar consumer offset timing issues? I'd be curious to hear how others model the commit window.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/3afb7968-1447-4973-8084-23956b998270n%40googlegroups.com.