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