Deductive Verification of Temporal Collisions in Distributed Message Brokers | Zenodo
Skip to main
You are using an outdated browser. Please upgrade your browser to improve your experience.
Planned intervention : We expect a short interruption on Monday, July 13th, at approximately 12:00 (UTC), due to a platform update.
Published July 10, 2026
| Version v1
Preprint
Open
Deductive Verification of Temporal Collisions in Distributed Message Brokers
Authors/Creators
Rochev, Illia
Description
Asynchronous message brokers with at-least-once delivery semantics—Apache Kafka, RabbitMQ, and NATS JetStream—exhibit a fundamental temporal collision: a consumer may crash between storing a result and committing the offset, causing duplicate execution upon redelivery. We present a formal verification study across all three brokers under four delivery modes using 12 TLA+ models and TLC model checking (108 configurations), cross-validated with Docker and Toxiproxy fault injection. Pulse-coupled synchronization is shown not to eliminate the crash window
Files
journal.pdf
Files<br>(372.2 kB)
Name<br>Size
Download all
journal.pdf
md5:873314f8f1258b08cc173b3beb1cdc7f
372.2 kB
Preview
Download
Views
Downloads
Show more details
All versions<br>This version
Views
Total views
Downloads
Total downloads
Data volume
Total data volume
0 Bytes<br>0 Bytes
More info on how stats are collected....
Versions
External resources
Indexed in
OpenAIRE
Communities
Keywords and subjects
Keywords
Asynchronous message broker
temporal collisions
formal verification
TLA+
model checking
Apache Kafka
RabbitMQ
NATS JetStream
Distributed Computing
Formal Methods
Details
DOI
DOI Badge
DOI
10.5281/zenodo.21298530
Markdown
[](https://doi.org/10.5281/zenodo.21298530)
reStructuredText
.. image:: https://zenodo.org/badge/DOI/10.5281/zenodo.21298530.svg<br>:target: https://doi.org/10.5281/zenodo.21298530
HTML
Image URL
https://zenodo.org/badge/DOI/10.5281/zenodo.21298530.svg
Target URL
https://doi.org/10.5281/zenodo.21298530
Resource type<br>Preprint
Publisher<br>Zenodo
Languages
English
Rights
Copyright
Copyright (C) 2026 Rochev Illia
Citation
Export
Technical metadata
Created
July 10, 2026
Modified
July 10, 2026
Jump up
This site uses cookies. Find out more on how we use cookies
Accept all cookies<br>Accept only essential cookies