La IA de Claude verifica 123 librerías reales

Claude ha generado pruebas matemáticas de seguridad para 123 librerías de código abierto, un experimento de Anthropic y Theorem que lleva la verificación formal desde proyectos muy especializados hasta software usado en el mundo real.

La verificación formal intenta demostrar que un programa cumple ciertas reglas en todos los casos contemplados, no solo en los ejemplos que alguien ha probado. En teoría, puede ofrecer garantías mucho más fuertes que ejecutar millones de pruebas. En la práctica, escribir esas demostraciones ha exigido años de trabajo experto.

Anthropic asegura que Claude consiguió automatizar buena parte de ese proceso. El modelo trabajó sobre los programas compilados, es decir, sobre las instrucciones que ejecuta el procesador, y no únicamente sobre el código fuente original.

Qué consiguió demostrar Claude

El equipo convirtió pruebas de seguridad ya existentes en una especificación formal. La regla era concreta: determinados programas no debían bloquearse, fallar una afirmación ni provocar errores de seguridad de memoria para ninguna entrada de menos de 64 MB.

Claude realizó este trabajo en 239 puntos de entrada pertenecientes a las 123 librerías. Un punto de entrada es la función o interfaz desde la que una prueba introduce datos en el programa. El análisis se hizo sobre binarios compilados para la arquitectura RISC-V, con un modelo formal del sistema operativo Linux.

Las garantías tienen condiciones importantes. Los programas se analizaron como binarios estáticos, de un solo hilo, con una cantidad fija de memoria y ejecutados sobre un procesador RISC-V. No significa que la misma prueba cubra automáticamente cómo funcionan esas librerías en ordenadores x86, dispositivos ARM o sistemas con bibliotecas enlazadas de otra manera.

Aun con esas limitaciones, el volumen es notable: las pruebas generadas suman alrededor de 180 millones de líneas de Rocq, el lenguaje y comprobador formal utilizado para revisar las demostraciones. Un comprobador independiente valida que la prueba satisface exactamente la especificación escrita.

También encontró errores antiguos

Claude no se limitó a intentar demostrar que el código era seguro. Cuando una prueba fallaba, el modelo investigaba el motivo, proponía un parche y volvía a ejecutar el proceso con la versión corregida.

Ese procedimiento descubrió cientos de errores, incluidos algunos que las herramientas tradicionales tenían pocas posibilidades de encontrar. Entre ellos había:

• Un desbordamiento de contador en un descompresor que podía provocar una escritura fuera de los límites con entradas de unos 20 MB y una disposición muy concreta.
• Una lectura fuera de límites en un decodificador de imágenes que requería una entrada de 64 MB y más de 2 GB de memoria.
• Un error que solo aparecía después de una secuencia específica de llamadas sobre dos manejadores del mismo archivo.
• Un fallo lógico que permitía cargar archivos aunque una función debía restringir qué archivos estaban permitidos.

El análisis también redescubrió la vulnerabilidad CVE-2026-56132 en libexpat, según Anthropic. Algunos de estos casos podían escapar a los fuzzers, herramientas que generan grandes cantidades de entradas modificadas para intentar provocar fallos. Probar muchas entradas ayuda, pero no garantiza recorrer todas las rutas posibles del programa.

Esto no significa que el software sea infalible

La diferencia es esencial: una prueba formal no demuestra que una librería esté libre de cualquier error. Demuestra que cumple una especificación concreta dentro de un modelo concreto de la máquina y bajo unas condiciones determinadas.

Si la especificación no describe algo importante, la prueba no lo cubrirá. Tampoco detectará un problema en el procesador, el sistema operativo o el propio modelo formal. Y demostrar que ciertos puntos de entrada no fallan no equivale a verificar cada función, cada uso posible de la librería o todo el programa que la utiliza.

En este experimento, además, la comprobación se centró en entradas de menos de 64 MB y en errores que podía detectar el sistema AddressSanitizer. Hay vulnerabilidades de memoria que esa herramienta no identifica, y una aplicación puede usar una librería de forma incorrecta aunque la librería haya superado sus pruebas.

Qué cambia para el desarrollo de software

Hasta ahora, la verificación formal se reservaba sobre todo para sistemas donde un fallo puede costar vidas o enormes cantidades de dinero. El propio equipo cita un caso conocido: verificar formalmente el núcleo seL4 requirió aproximadamente 20 años-persona, frente a los dos años-persona necesarios para implementarlo.

Si los modelos de IA reducen ese coste, las empresas podrían aplicar pruebas formales a componentes compartidos como bibliotecas de cifrado, compresores, lectores de documentos o herramientas de red. Una sola librería verificada podría aportar garantías reutilizables a miles de aplicaciones que dependen de ella.

Todavía hay un obstáculo práctico: generar estas pruebas consume cientos de millones de tokens y mucho tiempo de cómputo. Anthropic afirma que Opus 5.5 resolvió la mitad de un conjunto de 36 tareas usando alrededor de un 40 % menos de tokens que Opus 5. Cuando varios agentes compartieron pruebas parciales, necesitaron un 17 % menos de tokens que trabajando por separado.

El siguiente paso será acercar los modelos formales a los sistemas que realmente utilizas, incluidos procesadores x86 y ARM, bibliotecas dinámicas y programas con varios hilos. La promesa no es que Claude certifique cualquier aplicación con un clic, sino que la verificación deje de ser una tarea reservada a unos pocos especialistas y empiece a integrarse en el desarrollo normal, junto con las pruebas y el análisis de código.