A. Finn Hackett, Joshua Rowe, Markus Alexander Kuppe: Understanding Inconsistency in Azure Cosmos DB with TLA+. ICSE-SEIP 2023: 1-12