Verificación formal
Una demostración matemática de que un programa cumple su especificación — las pruebas muestran que hay errores, la verificación formal muestra que no los hay.
Asistentes de prueba: Coq (ahora Rocq, ~1989, Francia), Agda, Lean (Microsoft Research, impulsor de la revolución de 2024 en demostraciones matemáticas), Isabelle/HOL. Sistemas famosos demostrados: seL4 (el núcleo, 2009 — demostrado libre de una larga lista de clases clásicas de errores de kernel), CompCert (compilador de C, demostrado correcto), Project Everest (TLS verificado). Curvas de aprendizaje empinadas, meses o años para verificar programas sencillos — solo vale la pena para código muy crítico para la seguridad (aviación, energía nuclear, bibliotecas criptográficas).