Claude pone sus pruebas de software a examen

De probar ejemplos a demostrar una regla

Anthropic presenta un método que parte de las pruebas que los desarrolladores ya habían preparado. Esas pruebas reciben entradas y señalan ciertos errores haciendo que el programa falle. El trabajo transforma esa condición en una especificación matemática: demostrar que no se produce un fallo para ninguna entrada dentro del alcance definido.

Según la empresa, la diferencia respecto a generar muchas entradas de prueba está en la cobertura de la afirmación. Ejecutar ejemplos busca casos que rompan el programa, pero no garantiza recorrer todos los caminos posibles. Una demostración válida descarta los fallos contemplados a lo largo de cualquier camino alcanzable desde el punto de entrada, siempre dentro de sus condiciones.

Quién escribe la prueba y quién la acepta

Según Anthropic, la biblioteca y su prueba existente se compilan para obtener un ejecutable. A partir de ese ejecutable, los modelos formales y la propiedad de ausencia de fallos se genera la especificación que debe satisfacer la demostración. Claude escribe la prueba; el núcleo de Rocq comprueba que se ajusta a esa especificación.

Según la empresa, el volumen de las demostraciones no obliga a revisar manualmente cada línea. La confianza se concentra en los modelos de la máquina y del sistema operativo, los enunciados exactos demostrados y el propio comprobador. Esa separación permite verificar el resultado del modelo, pero mantiene componentes de confianza cuya corrección sigue siendo necesaria.

La garantía tiene un perímetro

Anthropic afirma que el resultado se refiere a los ejecutables compilados y a los puntos de entrada verificados. La garantía incluye la terminación normal, sin los errores de memoria y las aserciones fallidas contemplados, para las respuestas del sistema operativo y las distribuciones de memoria modeladas. Las condiciones de ejecución forman parte del resultado, no son detalles intercambiables.

Buscar errores mientras se construye la demostración

Anthropic afirma que los intentos de demostración descubrieron fallos que las pruebas automáticas difícilmente habrían encontrado. Algunos exigían entradas grandes con una estructura muy concreta o una secuencia particular de operaciones. El procedimiento permitía corregir el código, regenerar la especificación y continuar con la demostración sobre la versión modificada.

Según la empresa, esa capacidad de modificar el programa exigía vigilar los parches. Los investigadores penalizaron cualquier modificación y premiaron demostrar qué entradas cambiaban de comportamiento y que fueran pocas. También registraron y auditaron los parches para detectar atajos que cumplieran el objetivo formal a costa de alterar la tarea.

Lo que sigue fuera de la prueba

Según Anthropic, los ejecutables estudiados usan una arquitectura y una forma de enlazar las bibliotecas que difieren de muchas instalaciones reales. La prueba no se traslada automáticamente a otras máquinas o configuraciones. Además, el mecanismo que detecta errores de memoria no identifica todos los posibles: demostrar que sus alarmas no saltan no cubre errores que ese mecanismo no observa.

Anthropic sostiene que tampoco se verificaron todos los puntos de entrada de cada biblioteca. Incluso cubrirlos todos dejaría posibles huecos, como código no alcanzable desde ellos. Otra aplicación puede usar mal una biblioteca y corromper su propia memoria; cerrar ese hueco requiere especificar las obligaciones de quien llama a cada función y respetarlas.