TLA+ Modeling of AWS outage DNS race condition
On Oct 19–20, 2025, AWS’s N. Virginia region suffered a major DynamoDB outage triggered by a DNS automation defect that broke endpoint resolution. The issue cascaded into a region-wide failure lasting nearly a full day and disrupted many companies’ services. As with most large-scale outages, the “DNS automation defect” was only the trigger; deeper systemic fragilities ( see my post on the Metastable Failures in the Wild paper ) amplified the impact. This post focuses narrowly on the race condition at the core of the bug, which is best understood through TLA+ modeling. My TLA+ model builds on Waqas Younas’s Promela/Spin version . To get started quickly, I asked ChatGPT to translate his Promela model into TLA+, which turned out to be a helpful way to understand the system’s behavior, much more effective than reading the postmortem or prose descriptions of the race. The translation wasn’t perfect, but fixing it wasn’t hard. The translated model treated the enactor’s logic as a single atom...