La verificación formal permite demostrar matemáticamente que un programa cumple ciertas propiedades en todos los estados alcanzables, a diferencia del testing, que solo descarta un conjunto finito de casos. Para ello se usan lenguajes como Dafny, Lean, Rocq, Isabelle, F* o TLA+, en los que las especificaciones y las pruebas son ciudadanas de primera clase: se escriben contratos (precondiciones y postcondiciones) y un verificador externo, normalmente un solver SMT, comprueba de forma mecánica que el código satisface esas propiedades. Si la prueba falla, el código no compila. El artículo lo ilustra con un ejemplo en Dafny sobre el saldo de un carrito de compras: con unas pocas líneas se garantiza que el saldo nunca es negativo tras aplicar un cupón.
Históricamente, esta disciplina quedó confinada a la aviónica, los chips, los sistemas nucleares y la criptografía, porque redactar las pruebas era lento, tedioso y exigía perfiles muy especializados. La clave ahora es que los modelos de IA, desde Opus 4.5, saben proponer especificaciones formales a partir de requisitos en lenguaje natural, sugerir estrategias de demostración e iterar con el verificador cuando una prueba falla. La IA propone candidatos y el verificador, un proceso determinista, los valida uno a uno; la confianza se deposita así en la corrección de la especificación, no en el modelo. La consecuencia práctica es que la verificación formal deja de ser un lujo de sistemas críticos y se vuelve una opción razonable para cualquier software con reglas de negocio cuya corrección deba garantizarse, como sistemas de permisos, flujos de pedidos o lógica financiera.