- La verificación formal (formal verification) es un método para demostrar matemáticamente que el código siempre satisface una especificación, y durante mucho tiempo ha permanecido en un ámbito limitado y centrado en la investigación
- Algunos sistemas grandes, como el microkernel seL4, fueron desarrollados con verificación formal, pero por su alta complejidad y costo casi no se ha usado en la industria
- Recientemente, las herramientas de asistencia de programación basadas en LLM han mostrado resultados no solo en código de implementación, sino también en la redacción de scripts de prueba en varios lenguajes, lo que plantea la posibilidad de cambiar drásticamente la estructura de costos de la verificación
- Si la IA puede automatizar no solo la generación de código sino también la demostración de corrección, podría producirse una transición hacia una forma de desarrollo más confiable que la revisión humana de código
- La automatización de la verificación formal es una tecnología clave para asegurar la confiabilidad del software en la era de la IA, y se prevé que el factor decisivo para su adopción masiva será más un cambio cultural que una limitación técnica
Estado actual y límites de la verificación formal
- Los lenguajes y herramientas orientados a pruebas como Rocq, Isabelle, Lean, F*, Agda permiten demostrar matemáticamente que el código satisface una especificación
- Entre los casos representativos están el kernel del sistema operativo seL4, el compilador de C CompCert y el stack de protocolos criptográficos Project Everest
- Sin embargo, en la industria la verificación formal casi no se utiliza
- En el caso de seL4, verificar 8,700 líneas de código C requirió 20 años-persona y 200,000 líneas de código Isabelle
- Por cada línea de implementación se necesitan 23 líneas de prueba y medio día de trabajo humano
- Se estima que en todo el mundo hay apenas unos cientos de especialistas capaces de escribir este tipo de pruebas
- Desde el punto de vista económico, en la mayoría de los sistemas el costo de verificar supera las pérdidas causadas por bugs, por lo que su utilidad práctica ha sido limitada
Cómo la IA está cambiando la economía de la verificación formal
- Recientemente, los asistentes de programación basados en LLM han mostrado avances no solo en código de implementación, sino también en la redacción de scripts de prueba
- Nature, Galois y arXiv, entre otros, han reportado casos en los que los LLM generaron pruebas en varios lenguajes
- Hoy todavía se requiere la guía de expertos, pero se espera que la automatización total sea posible en pocos años
- Si el costo de la verificación cae con fuerza, será posible aplicar verificación formal a mucho más software
- Al mismo tiempo, el código generado por IA necesita garantizar su confiabilidad mediante verificación formal en lugar de revisión humana
- Si la IA puede demostrar por sí sola la corrección del código, podría llegar a preferirse frente al código escrito manualmente
Complementariedad entre los LLM y la verificación de pruebas
- Cuando un LLM redacta scripts de prueba, aunque genere contenido falso (alucinaciones), el proof checker lo rechaza
- El checker está compuesto por una pequeña base de código verificada por sí misma, por lo que es difícil que deje pasar una prueba incorrecta
- Por eso, la incertidumbre de los LLM se compensa con el rigor de la verificación formal
- Esta combinación funciona como una ruta segura de automatización para asegurar la confiabilidad del código generado por IA
Nuevo reto: la precisión al definir especificaciones
- Incluso en un entorno de verificación automatizada, definir correctamente la especificación (specification) sigue siendo la tarea central
- Hay que comprobar que la propiedad demostrada coincide realmente con la que el desarrollador pretendía
- Redactar especificaciones sigue requiriendo experiencia y pensamiento cuidadoso, pero es mucho más simple y rápido que hacer pruebas manuales
- La IA también podría ayudar con la traducción de especificaciones entre lenguaje natural y lenguaje formal
- Aun así, existe riesgo de pérdida de significado, aunque se considera manejable
Perspectiva de cambio en la forma de desarrollar software
- Los desarrolladores podrían pasar a describir las propiedades deseadas del código mediante especificaciones declarativas, y dejar que la IA genere tanto la implementación como la prueba
- En ese caso, no haría falta que los desarrolladores revisen directamente el código generado por la IA, y podría usarse sobre la base de la confianza, igual que el código máquina producido por un compilador
- En resumen, se prevén los siguientes tres cambios
- Una caída drástica en el costo de la verificación formal
- Un aumento en la demanda de verificación para asegurar la confiabilidad del código generado por IA
- La precisión de la verificación formal complementará la naturaleza probabilística de los LLM
- Si estos factores se combinan, es muy probable que la verificación formal se convierta en una tecnología dominante de la ingeniería de software
- Se prevé que, a futuro, el factor limitante no será la tecnología sino la velocidad con la que la cultura de desarrollo adopte el cambio
1 comentarios
Comentarios de Hacker News
Creo que la verificación formal (formal verification) realmente demuestra su valor en áreas donde la implementación es mucho más compleja que la especificación.
Por ejemplo, en lugares como optimizaciones a nivel de bits en implementaciones criptográficas o fases de optimización de compiladores.
Pero el código que escriben la mayoría de los desarrolladores (o la IA) ya está bastante cerca de la especificación gracias a los lenguajes de alto nivel, así que no creo que el beneficio de la verificación formal sea tan grande.
Incluso dudo que escribir una especificación por separado sea más legible.
Hoy en día muchos frameworks y librerías ya abstraen los detalles de implementación.
La verificación formal puede dar garantías más fuertes, pero la mayoría de la gente no quiere ese nivel de garantías, y no creo que la IA vaya a crear esa necesidad de la nada.
Algunas personas predicen que la IA automatizará por completo la verificación formal, pero yo veo problemas en esa lógica.
Si la IA pudiera demostrar software automáticamente, ni siquiera haría falta verificar software escrito por humanos.
La IA podría por sí sola concebir ideas, implementarlas y decidir el nivel de verificación.
Al final, es muy probable que desaparezcan tanto la programación como la verificación hechas por humanos.
En la práctica, es posible que humanos diseñen asistentes de prueba, pero verificar programas grandes con ellos es mucho más difícil.
Por eso, si apareciera una IA así, probablemente podría crear nuevos asistentes de prueba por su cuenta.
Claro, este tipo de especulación está más cerca de la ciencia ficción, y no tiene mucho sentido hacer predicciones cuando ni siquiera está claro qué cosas la IA hará más fáciles o más difíciles.
Enlace a la discusión relacionada
Siento que ese sería el punto de inflexión en el que la humanidad entraría en una etapa completamente distinta.
Para obtener resultados útiles con agentes de programación (Claude Code, Codex CLI, etc.), la clave es contar con un entorno donde puedan ejecutar y verificar el código que escriben.
Los lenguajes fáciles de ejecutar, como Python, son los más adecuados, y si se trata de HTML+JS hay que usar herramientas como Playwright.
El siguiente nivel es tener una suite de pruebas automatizadas, y después herramientas de calidad como formateadores, linters y fuzzers.
Los depuradores también son buenos, pero como son interactivos, a los agentes les cuesta manejarlos.
También creo que las herramientas de verificación formal entran dentro de este espectro, porque los modelos de hoy manejan bastante bien incluso lenguajes de programación especializados.
Si sientes que los agentes de programación no sirven mucho, probablemente sea porque te falta un entorno de ejecución y pruebas.
Si tomas Haskell como ejemplo, si compila, casi siempre funciona bien.
Si esa propiedad es útil para humanos, también lo será para los LLM.
En especial, los property test encajan muy bien con los LLM, porque con pocas pruebas puedes cubrir una región amplia de errores.
Viendo que en la comunidad matemática ya están intentando usar LLM para mejorar código en Lean, parece totalmente posible desarrollar software aprovechando sistemas de tipos más potentes.
La depuración no es secuencial, y los momentos de causa y efecto se mezclan.
Hace tiempo probé usar ChatGPT mientras perseguía un bug multihilo con gdb, pero solo repetía sugerencias simples como agregar prints.
Al final volví a sentir que esta es un área donde hacen falta experiencia e intuición.
No tiene sentido pedirle a un ingeniero junior que trabaje sin depurador ni ejecutor de pruebas.
Al final, parece que hará falta más capacidad de cómputo.
Claude implementa, y Codex y Gemini revisan.
Este método cuesta bastante, pero fue la forma más confiable de reducir el sesgo propio (self-bias) y mejorar la calidad del código.
Las herramientas de análisis estático podrían ayudar adicionalmente, pero siento que simplemente agregar más herramientas no basta.
Si se automatiza el proceso de verificación, la parte realmente difícil pasa a ser definir correctamente la especificación (specification).
Escribir la especificación es mucho más rápido y fácil que construir la prueba misma, pero aun así requiere especialización y cuidado.
Una razón por la que la prueba formal no se expandió en el pasado no fue solo su dificultad, sino también que desapareció el enfoque waterfall y pasó a dominar el desarrollo ágil.
En vez de escribir especificaciones largas, evolucionamos hacia iterar rápido según las necesidades del usuario.
Parece que ya es momento de aprender OCaml.
Muchos asistentes de prueba y sistemas de verificación pueden generar código OCaml, y ADA/Spark también vale la pena considerarlo.
La ingeniería de software en la era de la IA va a cambiar de una forma u otra, pero tendremos que crear software de mayor calidad que ahora.
La verificación formal claramente ayudará a lograr ese objetivo.
Todavía está incompleto, pero comparto mi proyecto experimental.
En un mundo con escasez de textos centrados en código, puede servirle a alguien que esté buscando una idea interesante para un hackatón.
Enlace al proyecto py-mcmas
Los LLM tienden a resolver bien los problemas que son fáciles de verificar.
Por eso yo divido la resolución en tres pasos.
1️⃣ Primero escribo un programa con la condición de éxito.
2️⃣ Luego hago que ese programa verifique el problema original.
3️⃣ Y al final yo mismo lo reviso.
Este enfoque lo he usado desde hace tiempo, pero ahora modelos como Opus o GPT-5.2 también lo hacen bien en modo no supervisado.
Entrada de blog relacionada
En áreas donde verificar toma mucho tiempo, incluso podrían aumentar la carga de validación para los humanos.
Puede surgir la pregunta: “¿y quién verifica el programa de verificación?”.
Si el LLM también escribe eso, puede parecer una torre infinita de tortugas (turtles all the way down).
Lo difícil es el proceso de construir la prueba.
Claro, hay excepciones en proposiciones complejas, pero aun así ayuda mucho a reducir bugs.
Aunque la verificación formal se popularice, no creo que todo el mundo vaya a usar Lean o Isabelle.
Más bien se expandirá en una forma donde la IA se integre de manera natural en los flujos de trabajo existentes.
Por ejemplo, verificación de propiedades en CI, o un botón en el IDE que diga “demostrar el invariante de este módulo”.
La mayoría de los ingenieros ni siquiera necesitará ver directamente los scripts de prueba.
Lo realmente difícil no es que el LLM produzca la prueba, sino conseguir que las organizaciones inviertan en escribir especificaciones y modelos.
Si la IA hace que proponer y revisar especificaciones sea fácil, la verificación terminará asentándose como una herramienta natural de refactorización, igual que las pruebas o los linters.
También hay gente que se queja de que GPT‑5.2 ni siquiera puede contar bien cuántas r tiene “garlic”.
Si de verdad lo necesitas, basta con pedirle al LLM que escriba y ejecute un script de Python.
Es cierto, pero no deja de ser un detalle de implementación de la tokenización, casi sin relación con la utilidad real.
Casi nunca hay motivo para usar un LLM para contar letras dentro de una palabra.