Claude lleva la verificación formal a 123 librerías

Claude demostró propiedades de seguridad directamente sobre el código ensamblador de 123 librerías de código abierto, cubriendo 239 puntos de entrada con pruebas que no requirieron intervención humana. La verificación formal —demostrar con matemáticas que un programa nunca viola una regla— dejó de ser un privilegio de la aviónica y pasó a ser una técnica que cualquier equipo de desarrollo puede empezar a explorar. Para un founder que hoy despliega código generado por IA, el cálculo cambia: la misma tecnología que introduce bugs puede, ahora, demostrar que no están.

Qué hizo Anthropic con Claude

Anthropic publicó el 22 de octubre una investigación hecha junto a Theorem, firma especializada en verificación formal. El equipo le pidió a Claude probar propiedades de seguridad sobre el código ya compilado de bibliotecas de código abierto, a nivel de instrucciones RISC-V. El resultado: 239 puntos de entrada en 123 librerías, casi todas parte de OSS-Fuzz, la iniciativa de fuzzing continuo de Google, quedaron con una prueba de que el programa siempre termina normalmente, sin errores de memoria ni aserciones fallidas, para cualquier entrada de menos de 64 MB y cualquier respuesta o distribución de memoria modelada del sistema operativo Linux.

Anthropic afirma que, según su conocimiento, es el primer esfuerzo a gran escala para aplicar verificación formal con IA a software de producción a nivel de ensamblador. Las pruebas se generaron en el transcurso de unas semanas.

El cambio de método es lo importante. Antes había que reescribir o modelar el código a mano. Ahora el proceso parte de los fuzz tests que los propios desarrolladores ya habían escrito: Claude convierte la regla de que ese test siempre pasa en una especificación formal sobre el binario compilado, y luego demuestra que se cumple.

Cómo se convierte un test en una prueba

El volumen da la medida de la dificultad. Según la cobertura de Unite.AI, Claude escribió alrededor de mil millones de líneas de Rocq durante el esfuerzo, de las cuales unos 180 millones pasaron el verificador de pruebas. Una prueba típica ronda las 600.000 líneas para garantizar binarios cuya mediana es de 18.000 instrucciones RISC-V. El parser de cJSON, con 391 líneas de código, recibió una prueba de 630.000 líneas.

¿Por qué tanto? Porque la verificación no se hace sobre el código fuente, sino sobre el comportamiento de la máquina. La prueba cubre todas las entradas posibles, todas las respuestas del sistema operativo y todas las distribuciones de memoria bajo los supuestos declarados. Para dimensionar el salto: el kernel seL4 tardó dos años-persona en implementarse y 20 años-persona en verificarse, el ejemplo clásico de por qué la técnica quedaba reservada a lo misionalmente crítico.

Un detalle clave: casi nada de ese código de prueba necesita revisión humana. El verificador Rocq comprueba que la prueba satisface la especificación. Lo único en lo que el desarrollador debe confiar es en los modelos formales de RISC-V y de los procesos de Linux, en los enunciados de los teoremas y en el propio verificador.

Los bugs que ni los fuzzers encontraban

El subproducto del proceso resultó tan valioso como el objetivo. Al intentar demostrar las propiedades, Claude encontró cientos de bugs y los fue parcheando para poder continuar. Muchos son casos que un fuzzer difícilmente habría detectado:

• Un subdesbordamiento de contador en un descompresor que provocaba una escritura fuera de límites, pero solo con entradas de unos 20 MB y una distribución muy poco frecuente.
• Una lectura fuera de límites en un decodificador de imágenes que necesitaba una entrada de 64 MB y más de 2 GB de memoria.
• Una lectura fuera de límites que exigía una secuencia concreta de llamadas a través de dos descriptores del mismo archivo.
• El redescubrimiento de CVE-2026-56132 en libexpat, que requiere entradas profundamente anidadas.

También aparecieron bugs de lógica que no cuelgan nada. Al probar la seguridad de memoria de una librería, Claude notó que una función que restringe qué archivos puede cargar una aplicación no siempre se aplicaba.

En otro experimento, durante un esfuerzo por verificar un lector de PDF ampliamente usado, el equipo encontró tantos bugs de seguridad en una semana como los que suelen reportarse en un año. Y en una aplicación crítica descubrió un bug de lógica desconocido que llevaba más de una década latente.

Por qué el contexto vuelve urgente esta técnica

El código que genera la IA hoy no es seguro por defecto, y eso está medido. El Veracode 2026 GenAI Code Security Report, analizado por ITUser, encontró que la tasa de aprobación en seguridad del código generado por IA sigue estancada en 56%, casi igual que el año anterior, mientras la tasa de compilación roza el 100%. Es decir: los modelos producen código que compila y funciona, pero vulnerable.

El informe, que analizó más de 100 modelos en cuatro series de pruebas y sin indicaciones específicas de seguridad, concluye que los modelos fallan en seguridad el 44% de las veces cuando no se les guía. Tampoco ayuda elegir un modelo especializado en programación: su tasa media es de 51% frente al 52% de los generalistas. El tamaño del modelo no cambia nada. La única ventaja significativa la tienen los modelos con capacidades de razonamiento, con 56% frente al 51%. Por lenguaje, Python llega al 63% y Java se queda en 30%.

El propio Chris Wysopal, cofundador de Veracode, lo resume así: el código generado por IA debe tratarse como cualquier otro código no revisado. El problema es de escala. El kernel de Linux, uno de los programas mejor testeados del mundo, tuvo más de 1.000 vulnerabilidades divulgadas en un período reciente. Si eso pasa con software auditado durante décadas, el código que tu equipo escribe esta semana no tiene ninguna posibilidad con tests solamente.

Los límites que Anthropic reconoce

Anthropic es explícito: formalmente verificado no significa sin bugs. Un verificador de pruebas no puede decirte si tu especificación refleja la realidad. Las garantías de este proyecto son condicionales:

• Las pruebas asumen binarios estáticos, de un solo hilo, enlazados contra musl libc y corriendo sobre RISC-V con Linux. La mayoría de la gente ejecuta esas librerías en x86 o ARM, con enlace dinámico contra glibc.
• AddressSanitizer no detecta todos los bugs de seguridad de memoria.
• No se verificaron todos los puntos de entrada de cada librería, y verificar los puntos de entrada tampoco cubre la librería completa.
• Un programa real puede usar mal la librería y corromper memoria en quien la llama.

La incertidumbre restante queda concentrada en los componentes de confianza: las semánticas de RISC-V y Linux, los enunciados de los teoremas y el verificador Rocq. No es poco, pero es una superficie muchísimo más chica que auditar cada línea de código de cada dependencia.

Cuánto cuesta probar: tokens y reutilización

El costo es el freno real. Generar estas pruebas puede consumir cientos de millones de tokens, y sin eficiencia esto no escala a todo el ecosistema. Anthropic midió dos palancas:

• Modelos mejores, menos tokens. En 36 tareas pequeñas de verificación construidas a partir de código real de OSS-Fuzz, Opus 5.5 resuelve la mitad con aproximadamente 40% menos tokens que Opus 5.
• Pruebas reutilizables. Cuando los agentes pudieron copiar las pruebas de otros en un espacio compartido, necesitaron 17% menos tokens que trabajando solos, y algunos lograron lo que antes no habían podido. A gran escala pasa lo mismo: buena parte de cada prueba cubre el runtime de C y la inicialización de AddressSanitizer, código que todos los programas comparten.

El precedente que Anthropic cita es Mathlib, la biblioteca de matemáticas formales en Lean, que creció hasta casi 300.000 teoremas aportados por más de 700 contribuyentes. Cada prueba nueva se apoya en las anteriores. Con las dependencias pasa lo mismo: siguen una ley de potencia, así que verificar un puñado de librerías compartidas habilita una franja enorme de software.

Theorem está ofreciendo el mismo pipeline gratis a proyectos open source a través de su programa OSS Verify, y su hoja de ruta apunta a verificar todo el ecosistema Nix, incluidos glibc, OpenSSL y cURL.

Qué significa esto para tu startup

1. Empieza por el inventario, no por la herramienta. Nadie va a verificar su producto entero. Las dependencias siguen una ley de potencia: identifica las cinco librerías de las que depende tu producto y que, si fallan, te dejan sin servicio. Esas son las candidatas.

2. Si tu producto es open source, prueba el pipeline de Theorem. El programa OSS Verify se solicita con un pull request que agrega tres archivos al repositorio del programa: project.yaml, Dockerfile y build.sh. Prioriza infraestructura crítica muy usada, los bugs que aparezcan se comunican en privado por correo a los mantenedores sin fecha límite de divulgación, y generar la prueba puede tardar varios días.

3. Trata el código de IA como código no revisado. Con una tasa de fallo en seguridad del 44% sin guía explícita, el código generado por tu equipo es tu principal superficie de riesgo. Revisión humana, análisis estático y tests con criterios de seguridad escritos no son opcionales.

4. Empieza a escribir especificaciones. El cuello de botella de la verificación no es la prueba, es definir qué significa que tu producto sea correcto. Documentar las reglas que tu software nunca puede violar es un trabajo que sirve hoy, aunque todavía no verifiques nada.

5. No confundas verificado con libre de bugs. Un proveedor que venda verificación formal como garantía absoluta está prometiendo algo que ni Anthropic reclama. La garantía vale exactamente lo que valen la especificación y el modelo de máquina que asume.

Conclusión

La verificación formal acaba de pasar de arte artesanal a pipeline automatizable. El dato que importa no es la cantidad de librerías cubiertas, sino que el costo de escribir pruebas cae a medida que los modelos mejoran y que las pruebas se pueden reutilizar. Ese es exactamente el patrón que siguió el testing cuando dejó de ser una tarea manual y se integró al ciclo de desarrollo.

Mientras tanto, la asimetría es incómoda: los atacantes ya usan IA para encontrar bugs a escala, y el código que escribimos con IA llega al mercado con una tasa de fallo en seguridad cercana a la mitad. Para un founder, la decisión práctica de esta semana es sencilla: saber de qué dependes y tratar cada línea generada por un modelo como si nadie la hubiera leído todavía.

Fuentes

• Anthropic – LLMs are making formal software verification feasible at a much larger scale (fuente original)
• Unite.AI – Anthropic Says Claude Proved Security Properties Across 123 Libraries
• Blockchain.News – Anthropic says Claude proved security properties in 123 open-source libraries
• ITUser – Casi la mitad del código generado por IA sigue sin superar las pruebas de seguridad

Artículos relacionados:

GPT-5.6 Luna vs GPT-6 Astra: ¿sirve el modelo barato para code review? Matthew Green: la IA hará que pidan puertas traseras al cifrado Google Chrome: 1.072 bugs corregidos con IA en junio 2026 Claude y rsync: ¿La IA aumenta los bugs? Un análisis lo desmiente Matthew Green: la IA podría dejar sin exploits a los gobiernos