Anthropic ha usado a Claude para algo que hasta ahora exigía años de trabajo de especialistas: demostrar con matemáticas que un programa cumple ciertas reglas de seguridad. Junto con la empresa Theorem, aplicó esta verificación formal a 123 bibliotecas de código abierto reales, directamente sobre el código ya compilado, y probó que sus pruebas automáticas no pueden fallar con ninguna entrada de menos de 64 MB. Por el camino, Claude encontró y corrigió cientos de fallos, algunos ocultos durante años.
Para entender por qué es importante, hay que distinguir entre probar y demostrar. La forma habitual de buscar fallos es el fuzzing: un programa lanza millones de entradas aleatorias contra el código y espera a que algo se rompa. Funciona, pero nunca es completo: siempre puede quedar una entrada que nadie probó. La verificación formal hace otra cosa: traduce el código a un modelo matemático y demuestra que se cumple una regla para todas las entradas posibles, sin excepción. Una vez demostrado, dentro de lo que cubre la demostración, ese tipo de fallo ya no hay que buscarlo: no existe.
El problema es el coste. Anthropic recuerda que el núcleo del sistema operativo seL4 costó dos años-persona de programar y veinte de verificar, y que por eso la técnica solo se usaba en código crítico, como el de la aviónica de Airbus. Y la urgencia es nueva: con la IA encontrando fallos cada vez más rápido, como pasó este mes con los de PHP, buscar fallos ya no basta. La pregunta es si se puede demostrar que no los hay.
Claves del trabajo de Anthropic y Theorem
- Qué demostraron: tomaron bibliotecas del proyecto OSS-Fuzz de Google, que somete a fuzzing continuo a cientos de programas de código abierto, y convirtieron sus pruebas en una regla matemática: «esta prueba nunca falla». Claude demostró que, para 239 puntos de entrada de 123 bibliotecas, el programa termina siempre con normalidad, sin errores de memoria ni comprobaciones fallidas, con cualquier entrada de menos de 64 MB.
- Sobre el código compilado: las demostraciones no se hicieron sobre el código fuente, sino sobre las instrucciones de máquina de un procesador RISC-V, que es lo que realmente se ejecuta. Ocupan unos 180 millones de líneas en Rocq, un lenguaje de demostraciones; una típica tiene unas 600,000 líneas. Nadie tiene que revisarlas a mano: un programa comprobador verifica que cada demostración es correcta.
- Cientos de fallos por el camino: cuando una demostración no salía, solía ser porque había un fallo real. Claude lo corregía y volvía a intentarlo. Anthropic cita varios que el fuzzing difícilmente habría encontrado: una escritura fuera de límites en un descompresor que solo aparecía con archivos de unos 20 MB con una estructura muy concreta, una lectura indebida en un decodificador de imágenes que necesitaba 64 MB de entrada y más de 2 GB de memoria, y el redescubrimiento de un fallo conocido de libexpat, la biblioteca de XML. También encontró errores lógicos que no provocan ningún fallo visible, como una restricción de archivos que no siempre se aplicaba.
- Más allá de la memoria: muchas pruebas de fuzzing comprueban propiedades útiles, como que comprimir y descomprimir devuelve lo mismo. Demostrar que la prueba no falla equivale a demostrar esa propiedad. En otros experimentos, Claude demostró que el zlib del kernel de Linux cumple el estándar del formato, y escribió un intérprete de Python en Rust que se comportó igual que CPython en el 99.95 % de 1.7 millones de programas de prueba. Al intentar verificar un lector de PDF muy usado, encontró en una semana tantos fallos de seguridad como se reportan en un año.
- Lo que reconocen como límites: «verificado formalmente no significa libre de fallos». Las demostraciones suponen un programa de un solo hilo en RISC-V y Linux, mientras que casi todo el mundo usa estas bibliotecas en x86 o ARM. No cubren todos los tipos de error de memoria ni todos los puntos de entrada de cada biblioteca. Y cada demostración consume cientos de millones de tokens, aunque Opus 5.5 ya necesita un 40 % menos que Opus 5 en las tareas de prueba.
De buscar fallos a demostrar que no los hay
Anthropic publica parte de las demostraciones para que cualquiera pueda revisarlas y reutilizarlas, aunque no las que podrían revelar un fallo aún sin parchear. Y Theorem ofrece hacer gratis lo mismo con otros proyectos de código abierto que cumplan sus requisitos, comunicando en privado a sus mantenedores los fallos que encuentre. Su hoja de ruta apunta a piezas sobre las que se apoya medio internet, como glibc, OpenSSL o cURL: como casi todo el software depende de las mismas bibliotecas, demostrar unas pocas protege a muchísimos programas.
Si se cumple lo que promete, la seguridad del software podría cambiar de lógica. Hasta ahora, defensores y atacantes competían por encontrar antes los fallos, y la IA está acelerando esa carrera por los dos lados, como vimos con el ataque a LiteLLM o con las claves de eMudhra. La verificación formal a gran escala ofrece algo distinto: dejar de buscar en ciertos tipos de fallo porque está demostrado que no existen. Todavía es cara y tiene límites claros, pero Anthropic cree que acabará siendo tan habitual como hoy lo es el fuzzing.
Más fuentes: programa de verificación gratuita de Theorem para proyectos de código abierto y demostraciones publicadas. Imagen de portada: Anthropic.