Anthropic lleva Claude a la verificación formal de 123 bibliotecas abiertas
Anthropic y Theorem dicen que Claude produjo pruebas formales para 239 puntos de entrada de 123 bibliotecas de OSS-Fuzz, al nivel de instrucciones RISC-V. El resultado cubre propiedades concretas bajo un modelo limitado de ejecución: no certifica bibliotecas enteras ni las vuelve libres de errores.
Anthropic y Theorem afirman que Claude ayudó a verificar propiedades de seguridad en 123 bibliotecas de código abierto. El sistema produjo pruebas para 239 puntos de entrada del catálogo OSS-Fuzz y, durante el trabajo, detectó y corrigió cientos de errores. La afirmación fuerte tiene una frontera igual de importante: se refiere a programas compilados para RISC-V, bajo condiciones descritas por los investigadores, no a una garantía general de que esas bibliotecas sean seguras en cualquier uso.
El experimento intenta convertir una técnica de pruebas conocida como fuzzing en una afirmación más amplia y comprobable. En el fuzzing, un programa recibe muchísimas entradas generadas o mutadas para encontrar alguna que lo haga fallar; si no falla, solo sabemos que sobrevivió a esas pruebas. Una demostración formal busca mostrar que una propiedad especificada se cumple para todas las entradas incluidas en un dominio definido.
-IA Crew dice: El fuzzer busca la aguja entre entradas al azar; la prueba formal intenta demostrar que, dentro del mapa acordado, no queda ninguna.-
Del test al código máquina
El equipo partió de los puntos de entrada que ya usaba OSS-Fuzz, donde una entrada puede hacer que una biblioteca se bloquee o active una aserción. Anthropic y Theorem transformaron el comportamiento esperado de esos tests en una especificación formal: para cada caso, el programa debe terminar sin fallos ni errores de seguridad de memoria. Esa elección acota la pregunta. La prueba puede certificar que el test no encuentra cierto tipo de fallo, pero no demuestra que la especificación cubra cada comportamiento que un usuario espera de la biblioteca.
Después, Claude escribió las pruebas sobre el ejecutable compilado para RISC-V. El kernel de Rocq, un verificador que comprueba mecánicamente las demostraciones contra su especificación, revisó esos desarrollos. La colaboración produjo unos 180 millones de líneas de prueba; el artículo de Anthropic indica que una prueba típica rondaba las 600.000 líneas para binarios de una mediana de 18.000 instrucciones. Es volumen generado por la máquina, no una pila que un mantenedor tenga que leer línea por línea para confiar en cada inferencia.
-IA Crew dice: Si alguien imprime las 180 millones de líneas para revisarlas a mano, el problema ya no es de verificación: es de papelería.-
La propiedad probada tiene límites concretos. Los programas se modelaron como binarios estáticos de un solo hilo, con memoria fija, ejecutados en un procesador RISC-V con Linux; las entradas consideradas eran menores de 64 megabytes. Bajo esos supuestos, Claude llegó a demostrar que 239 puntos de entrada de las 123 bibliotecas podían terminar normalmente sin los fallos contemplados. No es una prueba de todas las rutas, procesadores, sistemas operativos o configuraciones que esas bibliotecas pueden encontrar fuera del modelo.
Lo que queda fuera de la garantía
La búsqueda de demostraciones sirvió además para encontrar errores difíciles de reproducir con pruebas aleatorias. Anthropic describe, entre otros, un desbordamiento que conducía a una escritura fuera de límites y solo aparecía con una entrada cercana a 20 megabytes y una distribución poco común. También informa de cientos de fallos encontrados y corregidos durante el proceso. Es un resultado útil incluso cuando no se completa una prueba: el intento puede revelar un caso que los tests anteriores no habían alcanzado.
Sin embargo, “verificado” no significa “libre de errores”. Una demostración certifica que el ejecutable satisface el enunciado matemático, siempre que sean correctos el modelo de RISC-V y Linux, la especificación y el propio verificador. Si el enunciado omite una propiedad importante o el modelo no refleja el entorno real, la prueba no detectará ese hueco. Anthropic reconoce expresamente esta dependencia y ha publicado solo una parte de las pruebas y los componentes de confianza para que otras personas puedan revisarlos.
El paso interesante es de escala: automatizar buena parte de una tarea que antes exigía especialistas y mucho tiempo. La parte menos vistosa —definir exactamente qué se quiere probar y confiar en los modelos de la máquina— sigue siendo trabajo de ingeniería. Si el método se extiende a más arquitecturas y sistemas operativos, podría ayudar a endurecer dependencias compartidas; si no, sus resultados seguirán siendo valiosos, pero circunscritos a los binarios y supuestos estudiados.
-IA Crew dice: La máquina puede certificar un teorema impecable; todavía hay que comprobar que le dimos el problema correcto.-
Diccionario de la Crew
Fuzzing — Técnica que prueba un programa con muchas entradas generadas o modificadas para descubrir fallos.
Especificación formal — Enunciado matemático preciso de la propiedad que debe cumplir un programa.
Rocq — Asistente de demostración cuyo kernel comprueba que una prueba satisface su especificación.
