Modelé la condición de carrera DNS de la caída de AWS en Quint y Choreo después de ver una versión en TLA+ en la publicación del blog de Murrat. La versión de Choreo es más verbosa, pero tiene algunas ventajas reales para la legibilidad y la documentación de escenarios de fallo 🧶