Investigadores de Stanford demostraron recientemente que una herramienta de inteligencia artificial puede completar un proyecto de ingeniería en menos de medio día, una tarea que tres expertos tardaron cinco meses en resolver de forma manual. El hallazgo reavivó el interés en un campo técnico de décadas de antigüedad: la verificación formal, una disciplina matemática que busca demostrar con precisión lógica que un programa de software no contiene errores.
A diferencia de las pruebas convencionales —que identifican fallos conocidos pero no garantizan ausencia total de defectos—, la verificación formal convierte el código en fórmulas matemáticas que pueden validarse de manera exhaustiva. El proceso históricamente ha sido tan costoso y especializado que su adopción quedó limitada a entornos de misión crítica, como los sistemas de la NASA o ciertos componentes de Apple. Hoy, un grupo de startups financiadas con capital significativo está apostando a que la IA generativa cambia esa ecuación.
Capital y casos de uso que marcan el ritmo
Entre las empresas que están construyendo sobre esta premisa destaca &Truth, que ha recaudado 70 millones de dólares y tiene como objetivo verificar código escrito en cualquier lenguaje de programación. Su investigadora Chuyue Sun utilizó IA para verificar parte del código que encripta las conversaciones en la aplicación de mensajería Signal, un caso de uso con implicaciones directas para la seguridad de datos a escala masiva.
Harmonic, que cuenta con 295 millones de dólares en financiamiento, anunció esta semana que su agente de IA —denominado Aristotle— ya soporta verificación de software escrito en C y diseños de hardware en Verilog. La compañía está evaluando la tecnología con fabricantes de chips como Tensordyne y Nvidia, cuyo brazo de capital de riesgo figura entre sus inversores. En paralelo, Anthropic y la startup Theorem anunciaron que utilizaron IA para detectar errores en software de código abierto que billones de pruebas convencionales no habían logrado identificar, además de presentar un complemento para el modelo Claude orientado a facilitar la verificación a otros desarrolladores.
Por qué la adopción generalizada sigue siendo un desafío
A pesar del impulso financiero y técnico, la pregunta central persiste: ¿puede la verificación formal escalar más allá de los sistemas más críticos y convertirse en una práctica estándar de desarrollo de software? La respuesta tiene implicaciones directas para cualquier organización que dependa de infraestructura digital, desde servicios financieros hasta manufactura conectada.
Ilya Sergey, director científico de &Truth, resume el argumento de fondo: los puentes y edificios no colapsan porque se aplican matemáticas antes de construirlos. El mismo principio, trasladado al software, podría reducir de forma estructural los costos asociados a vulnerabilidades de seguridad, tiempo de inactividad y corrección de errores en producción. La tecnología para razonar matemáticamente sobre el código ya existía; el reto siempre fue la escalabilidad. La IA generativa es, por ahora, la apuesta más concreta para resolverlo.
