Anthropic y Theorem utilizan Claude para generar demostraciones matemáticas sobre código compilado y detectar errores difíciles de encontrar mediante pruebas convencionales, con garantías sujetas a condiciones específicas.
El problema de probar software mediante la ejecución
Un programa puede superar millones de pruebas y conservar errores que todavía nadie ha conseguido activar.
Los desarrolladores utilizan pruebas automáticas para comprobar cómo responde el software ante distintas situaciones. También recurren al fuzzing, una técnica que genera y modifica grandes cantidades de datos para buscar comportamientos inesperados.
Estas herramientas son fundamentales, pero sus resultados tienen un límite: no encontrar un fallo no demuestra que ese fallo sea imposible.
Imagina un lector de imágenes que funciona correctamente con todos los archivos utilizados durante su desarrollo. Una combinación poco habitual de dimensiones, metadatos y contenido podría llevarlo a una situación que las pruebas anteriores nunca habían alcanzado.
Además, que un programa no se cierre inesperadamente tampoco basta para considerarlo seguro. Puede seguir funcionando mientras interpreta mal un permiso, muestra información indebida o realiza una operación incorrecta.
El reto consiste en avanzar desde comprobar ejemplos concretos hasta justificar que determinadas clases de errores no pueden producirse dentro de unas condiciones definidas.
Una alternativa matemática: la verificación formal
La verificación formal permite demostrar que un modelo del programa cumple una propiedad expresada mediante reglas matemáticas.
El punto de partida es definir con precisión qué se quiere garantizar. No basta con pedir que el software sea seguro: hay que convertir esa intención en una afirmación que pueda comprobarse.
El 22 de octubre de 2026, Anthropic presentó una colaboración con Theorem en la que Claude generó pruebas para 239 puntos de entrada de 123 bibliotecas de OSS-Fuzz.
Según la compañía, el trabajo se completó durante varias semanas e incluyó la corrección de errores encontrados durante el proceso.
El avance reside en ampliar la producción de demostraciones, una tarea especializada que puede exigir mucho esfuerzo. No equivale a haber resuelto todos los problemas de seguridad de esos proyectos.
¿Cómo funciona esto y qué implica para el usuario?
Para entender la diferencia, podemos imaginar las pruebas de resistencia de un puente.
Hacer pasar vehículos permite observar cómo responde la estructura en situaciones reales. Es una comprobación valiosa, pero cada ensayo cubre unas condiciones determinadas.
Un análisis matemático permite razonar sobre una familia completa de situaciones, siempre que el modelo represente correctamente los materiales, la estructura y las cargas contempladas.
Eso no garantiza que el puente soporte cualquier peso imaginable ni que sobreviva a circunstancias excluidas del cálculo. La garantía depende de lo que se haya definido y demostrado.
En software ocurre algo parecido. Una prueba formal puede establecer que una operación respeta una regla para todas las entradas incluidas en su alcance, en lugar de comprobar únicamente una selección de ejemplos.
Para el usuario, la ventaja potencial es que ciertos comportamientos peligrosos queden descartados antes de utilizar la aplicación. Pero esa protección debe describirse con precisión: una garantía sobre una función no convierte automáticamente todo el producto en invulnerable.
El reto del código a muy bajo nivel
El proyecto trabajó con ejecutables RISC-V bajo un modelo de Linux. Las garantías anunciadas incluyen límites como entradas inferiores a 64 MB, ejecución de un solo hilo y un presupuesto de memoria fijado.
RISC-V es una arquitectura de instrucciones: define las operaciones que puede realizar un procesador compatible. El ensamblador representa esas instrucciones de forma legible para las personas; el procesador ejecuta su codificación binaria.
Esta distinción importa porque el código que escribe un desarrollador pasa por transformaciones antes de ejecutarse. Trabajar sobre un binario permite analizar ese artefacto concreto.
Theorem plantea la verificación a nivel binario como una forma de abordar programas escritos en distintos lenguajes y construidos con diferentes herramientas.
Sin embargo, una demostración sobre una compilación determinada no debe trasladarse sin más a otra arquitectura, otra versión o un entorno diferente.
Pensemos en una pieza industrial: haber certificado un diseño bajo unas condiciones no certifica automáticamente todas sus variantes. Al modificarlo, hay que comprobar si el razonamiento sigue siendo válido.
Hallazgos en bibliotecas de código abierto
Anthropic comunica que el proceso permitió descubrir cientos de errores. Entre los ejemplos describe una escritura fuera de los límites de memoria que necesitaba una entrada de unos 20 MB con una disposición muy específica.
Este tipo de caso ayuda a entender por qué resulta difícil explorar todas las posibilidades ejecutando pruebas. El problema puede depender simultáneamente del tamaño de los datos, su organización y el estado previo del programa.
No obstante, que un agente no consiga completar una demostración no confirma por sí solo una vulnerabilidad. También puede faltarle una estrategia adecuada, información suficiente o recursos para terminar.
Hay que distinguir entre una prueba pendiente, un comportamiento incorrecto reproducible y una vulnerabilidad explotable. Son resultados diferentes y requieren evaluaciones diferentes.
Del mismo modo, encontrar un fallo mediante razonamiento formal no significa que ninguna otra técnica pudiera descubrirlo. Lo relevante es ampliar las formas de detectar problemas y justificar las correcciones.
Puntos clave del avance en ciberseguridad
- Automatización del razonamiento: La IA puede ayudar a construir demostraciones extensas, reduciendo parte del trabajo manual necesario para expresar y resolver obligaciones de prueba.
- Garantías concretas: El valor está en indicar qué propiedad se ha demostrado, sobre qué programa y bajo qué condiciones.
- Análisis del ejecutable: Trabajar con binarios permite vincular la demostración al código compilado que se está examinando.
- Comprobación independiente: En el repositorio publicado, las pruebas se verifican con Rocq y se expresan sobre un modelo formal de procesos Linux y binarios RISC-V.
- Reutilización del trabajo: Theorem propone construir verificaciones sobre componentes compartidos ya demostrados, evitando repetir desde cero el análisis de las mismas dependencias.
Límites reales y mitigación de riesgos
Una demostración matemática responde a una pregunta formal. Elegir bien esa pregunta sigue siendo una responsabilidad esencial.
Por ejemplo, demostrar que un proceso no se bloquea no demuestra necesariamente que solo puedan utilizarlo las personas autorizadas. Y demostrar que devuelve un resultado no implica que ese resultado sea el que necesita el usuario.
La documentación pública del proyecto advierte de que su modelo de Linux es incompleto y contiene supuestos. Las pruebas corresponden a binarios y enunciados específicos, con condiciones sobre memoria y comportamiento del entorno.
Esto obliga a revisar la cadena completa: qué se afirma, cómo se representa la máquina y qué componentes se consideran fiables.
También hay que comprobar las modificaciones realizadas durante el proceso. Un cambio que evita un fallo eliminando una función necesaria puede satisfacer una condición estrecha y, aun así, empeorar el programa.
La validación matemática y la revisión del comportamiento esperado deben trabajar juntas. El objetivo es conservar la utilidad del software mientras se refuerzan sus garantías.
Además, Anthropic reconoce que generar estas pruebas puede consumir cientos de millones de tokens. No hay base para afirmar que cualquier proyecto pueda convertir años de verificación en unas pocas horas a bajo coste.
El impacto a largo plazo en el software cotidiano
Muchas aplicaciones comparten componentes para procesar imágenes, leer documentos, comprimir archivos o intercambiar datos. Mejorar una dependencia utilizada por numerosos proyectos puede beneficiar a todos ellos.
La propuesta de Theorem parte de esa estructura compartida: verificar componentes fundamentales y reutilizar sus resultados al analizar programas que dependen de ellos.
Para los equipos de desarrollo, una adopción práctica podría empezar por funciones pequeñas y bien delimitadas, con propiedades claras y una utilidad evidente.
Por ejemplo, antes de intentar demostrar el comportamiento completo de un gestor documental, tendría sentido identificar qué operaciones críticas merecen garantías adicionales y cómo se integran con el resto del sistema.
Las pruebas tradicionales seguirían aportando información sobre integración, experiencia de uso y comportamiento en entornos reales. La verificación formal añadiría otra capa de evidencia allí donde su alcance esté bien definido.
El horizonte más interesante es que las aplicaciones puedan incorporar garantías verificables junto a su código, con una explicación clara de lo que cubren y de lo que queda pendiente.
La IA puede facilitar la construcción de esas garantías. Su valor dependerá de que sean correctas, pertinentes y aplicables al software que finalmente utiliza la gente.
Fuentes de información
- Anthropic Research: LLMs are making formal software verification feasible at a much larger scale.
- Theorem: repositorio de demostraciones, condiciones y límites de OSS Verify.
- Theorem: Bootstrapping the Verified Software Stack.
Sombra Radio · Apoyo de lectores
Ayuda a mantener viva Sombra Radio
Tu aportación voluntaria nos ayuda a seguir publicando sobre IA. Puedes apoyarnos desde 1 € al mes.
