Verificación de Programas en la Era de la IA: Por Qué las Alucinaciones Hacen que la Verificación de Código sea Más Importante

La IA generativa revivió un antiguo sueño de los programadores: simplemente formule una tarea — y la máquina escribirá el código por sí sola. Un nuevo estudio académico enfría este optimismo, sin negar el progreso real: la programación representa solo una pequeña parte de la ingeniería de software, y sus partes más difíciles — requisitos, arquitectura y verificación — aún permanecen con los ingenieros.

Por Qué la IA No Resuelve el Problema Principal

La ingeniería de software no es solo escribir código. Las encuestas de la industria muestran: los desarrolladores dedican del 20 al 30% de su tiempo de trabajo a la programación directa. El resto se dedica a la recopilación de requisitos, el diseño de arquitectura, la revisión, las pruebas y la corrección de errores. Los asistentes de IA pueden generar funciones y explicar código desconocido, pero no pueden probar la corrección del sistema en su conjunto — esta es una tarea fundamentalmente diferente.

El problema principal son las alucinaciones. La IA ofrece con confianza código que parece plausible, se compila y pasa pruebas básicas, pero contiene errores lógicos sutiles. Los componentes "casi correctos" apilados juntos forman un sistema poco confiable. Los autores recopilaron incidentes documentados con código generado por IA en producción: desde citas legales incorrectas en chatbots hasta errores en algoritmos de recomendación médica. El patrón es el mismo: el sistema funcionaba correctamente en la mayoría de los casos — hasta que encontraba un caso límite.

Experimento con AutoProof y Eiffel

Los investigadores no se limitaron a la teoría y realizaron un experimento concreto. Un sistema de gestión de conferencias se creó con la ayuda de un asistente de IA junto con AutoProof — un verificador formal para el lenguaje Eiffel. La diferencia fundamental respecto a las pruebas: la verificación formal prueba la corrección para todas las entradas posibles, no solo para un conjunto de ejemplos seleccionados.

El proceso requería disciplina iterativa rigurosa:

• Formular un pequeño fragmento de requisitos como precondiciones y poscondiciones formales
• Pedir al asistente de IA que implemente el código correspondiente
• Ejecutar AutoProof y obtener un error de verificación o confirmación de corrección
• Corregir la especificación o la implementación — y repetir el ciclo

Observación clave: el asistente de IA no verificó el código de forma independiente. Ayudó a formular especificaciones e implementar el código, mientras que un verificador formal independiente comprobaba la corrección. Esta división de roles es fundamental — y, según los autores, así es como se organizarán las cadenas de herramientas de próxima generación.

Federación de Agentes como Nuevo Paradigma

Los autores proponen una nueva perspectiva sobre el desarrollo: no un único asistente de IA, sino una federación de agentes que interactúan con zonas claras de responsabilidad. Uno genera código, un segundo escribe pruebas, un tercero ejecuta verificación formal, un cuarto analiza incidentes de producción. Ningún agente es completamente responsable de la corrección — es una propiedad del sistema en su conjunto.

"La alucinación como un tipo de fallo hace que las garantías de

corrección sean más, no menos importantes", argumentan los autores.

Este enfoque requiere que los desarrolladores entiendan la ingeniería de software clásica: especificaciones formales, invariantes, contratos. La IA no elimina este conocimiento — hace que su aplicación práctica sea más accesible. Un desarrollador que puede formular requisitos con precisión y leer resultados de verificación está en una posición fundamentalmente ventajosa.

Qué Significa Esto

La conclusión de los autores es cautelosamente optimista. Para el desarrollo cotidiano, la IA es una tecnología de nivelación: un desarrollador sin experiencia se aproxima a uno experimentado, el código rutinario se escribe más rápidamente, los errores obvios se encuentran antes. Para sistemas críticos y empresariales, la IA se convierte en una tecnología amplificadora: un ingeniero experimentado obtiene una herramienta poderosa, pero las lecciones clásicas de la ingeniería de software se aplican más que nunca. La verificación se vuelve no menos, sino más importante — precisamente porque la IA puede cometer errores con confianza e invisibilidad.