Hi Neil,
Thank you for the sharp critique — these are important points worth addressing.
On “horribly designed systems”: I agree. The prevalence of temporal collision bugs in production systems (documented across all four brokers) is itself evidence that the bus decoupling pattern is widely misapplied. Our paper explicitly calls this out: the fix is not better idempotency guards but better system design where the consumer’s processing is within the transaction boundary.
On “you must verify every service”: Correct, and our models do exactly this. The TLA+ specifications model the full protocol — not just the broker, but the consumer’s store-before-commit path as well. The invariant execCount ≤ 1spans both the consumer and broker state machines. That said, our models necessarily abstract away everything outside this protocol boundary, which is a deliberate scope choice, not a claim of completeness.
On “the protocol is the same, only variable names change”: This is the strongest critique and fair. What I should have said more precisely: the protocol pattern — process → store → crash-before-commit → redeliver → duplicate execution — is structurally identical across brokers because it follows from the at-least-once delivery contract itself, not from any broker-specific implementation detail. The variable names change (offset vs. seqno vs. deliveryTag), but the state machine shape (Ready → Processing → Stored → Crashed → Redelivered) and the crash window between Store and Commit are the same. Whether this constitutes an “invariant” in the TLA+ sense is debatable — it’s more accurately a structural property of the protocol class. Our paper formalizes each broker independently and then observes the structural isomorphism, rather than assuming it a priori.
On TLA+ for thinking vs. verification: I think you and Lamport would agree that our approach aligns with his intent — we use TLA+ to first prove the collision exists structurally (via exhaustive state-space exploration), then cross-validate with physical fault injection. The 16 templates are not “verified implementations”; they are formal arguments that a specific property holds (or fails to hold) under all possible interleavings. The chaos experiments then confirm the model’s predictions match physical reality. This two-layer approach — deductive proof plus empirical confirmation — is closer to how formal methods should be applied in practice.
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 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 that 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.