Un equipo de investigadores ha demostrado que los modelos de lenguaje de gran escala (LLMs) pueden generar pruebas formales de seguridad para software de producción a gran escala, eliminando la barrera histórica de la complejidad humana. En colaboración con Theorem, los autores utilizaron Claude para verificar propiedades de seguridad en más de 100 bibliotecas de código abierto, incluyendo artefactos compilados en RISC-V. Este trabajo marca el primer intento a gran escala de aplicar la verificación formal a software de producción mediante inteligencia artificial.
La verificación formal permite demostrar matemáticamente que el código está libre de errores que violen reglas de seguridad definidas. Tradicionalmente, este proceso requería años de esfuerzo experto y era viable solo en aplicaciones críticas, como los sistemas de aviónica de Airbus o el kernel seL4. Sin embargo, los LLMs actuales pueden generar estas pruebas de forma autónoma. En el experimento, Claude demostró que ciertos programas no causan errores de seguridad ni se detienen bajo condiciones específicas, como ejecuciones de un solo hilo en un sistema operativo Linux. Además, el modelo descubrió bugs que habían evadido la detección durante años, a pesar de millones de pruebas de estrés.
El equipo ha publicado un subconjunto de estas pruebas y las semánticas de RISC-V para permitir su verificación independiente. Theorem ofrece una herramienta para aplicar este pipeline a otros proyectos de código abierto. Esta innovación reduce el costo de la verificación formal, haciendo que la garantía de seguridad sea más accesible para el desarrollo de software moderno.