Modélisé la condition de course DNS de la panne AWS dans Quint et Choreo après avoir vu une version TLA+ dans le billet de blog de Murrat. La version Choreo est plus verbeuse, mais elle présente de réels avantages pour la lisibilité et la documentation des scénarios d'échec 🧶