Los métodos formales —herramientas matemáticas para especificar y verificar software— apenas se utilizan fuera de nichos académicos y de alta seguridad. Un análisis extenso repasa las razones históricas y estructurales de esta baja adopción y propone una mirada más matizada que los tópicos habituales de "es muy caro" o "no es un avión".
El texto diferencia entre especificación formal (cómo describir con precisión qué debe hacer un sistema) y verificación formal (cómo demostrar que el software cumple esa descripción), y separa además la verificación de código de la de diseño. En la práctica, ambos mundos usan lenguajes, herramientas y comunidades distintas, lo que fragmenta el campo.
En el terreno de la verificación de código, el artículo repasa los tres grandes enfoques para escribir especificaciones: teoremas independientes del programa (Isabelle, ACL2), aserciones y pre/postcondiciones embebidas (Dafny, SPARK, Eiffel con Diseño por Contrato) y sistemas de tipos dependientes (Coq, Agda). Estos tres estilos se corresponden, respectivamente, con tests, contratos y tipos en el espectro más amplio de comprobaciones de corrección, lo que ayuda a entender la verificación formal como el extremo más riguroso de un continuo, no como una técnica aislada.
Uno de los mayores obstáculos no es técnico sino conceptual: conseguir la especificación correcta. El autor distingue entre validación (demostrar que la especificación refleja lo que quiere el cliente) y verificación (demostrar que el código cumple esa especificación). Aun cuando el cliente itera rápido sobre sus requisitos, siempre hay propiedades que se dan por sentadas —que el programa no se caiga, que no tenga agujeros de seguridad— y que pueden formalizarse. Además, trasladar conceptos humanos a términos matemáticos exige una habilidad que se aprende con la práctica, igual que programar.
El recorrido continúa explorando por qué, pese a décadas de avances, la verificación formal de código sigue circunscrita a sectores como el aeroespacial o el ferroviario, y qué condiciones harían viable su expansión al software cotidiano.