gnatprove

Bend 2 se presenta como el lenguaje ideal para la era de la IA: los humanos escriben leyes, la IA escribe las pruebas. Pero para demostrar que un jugador nunca toca una bandera necesita 442 líneas de prueba, mientras SPARK, un lenguaje de verificación formal con décadas de historia, resuelve lo mismo en 12 checks automáticos. El caso expone una trampa clásica del vibe-coding: construir mucho antes de investigar si ya existe una solución mejor.