LLM y verificación formal: qué significa «demostrado» en 123 bibliotecas

El 22 de octubre de 2026, el Frontier Red Team de Anthropic, junto con una empresa llamada Theorem, publicó un resultado que vale la pena leer con calma. Usaron Claude para escribir pruebas formales sobre código abierto real, a nivel de ensamblador, en 123 bibliotecas, y por el camino encontraron bugs que habían sobrevivido a años de pruebas. Esto es lo que significa en palabras sencillas, dónde se acaba la palabra «demostrado» y qué puede sacar hoy un equipo normal.

La verificación formal, sin jerga

Un test comprueba las entradas que se te ocurrieron. Una demostración cubre todas las entradas. En la verificación formal conviertes el código en un modelo matemático, escribes reglas que siempre debe cumplir e intentas demostrar que el modelo las cumple. Si la demostración falla, la forma en que falla señala un posible bug. Lo corriges, lo intentas de nuevo y terminas con la prueba de que no queda ningún bug que rompa esas reglas.

El problema siempre ha sido el coste. El artículo da el ejemplo clásico: el núcleo seL4 necesitó dos años-persona para construirse y 20 para verificarse. Por eso la verificación se quedó en ámbitos como el código de aviónica.

Qué hicieron exactamente

Escribir la especificación suele ser lo más difícil, así que reutilizaron una que ya existía: los fuzz tests de OSS-Fuzz, de Google. Un fuzz test es un punto de entrada que falla cuando algo va mal, y un fuzzer le lanza cantidades enormes de entradas generadas. Puede funcionar durante años sin llegar nunca a ser completo. El equipo convirtió cada fuzz test en un enunciado: este punto de entrada nunca falla, para ninguna entrada de menos de 64 MB, en el binario RISC-V compilado.

En unas pocas semanas, Claude corrigió los bugs que encontró y demostró ese enunciado para 239 puntos de entrada en 123 bibliotecas. Las pruebas suman unos 180 millones de líneas de Rocq; una típica ronda las 600.000 líneas, para binarios con una mediana de 18.000 instrucciones RISC-V. Nadie lee eso a mano. Lo hace el verificador de pruebas de Rocq, y el artículo enumera lo que todavía hay que creer: los modelos formales de RISC-V y de los procesos de Linux, los enunciados exactos de los teoremas y el propio verificador.

Lo que hay que mirar son los bugs

Los fuzzers mutan entradas pequeñas, normalmente limitadas a 1 MB. Parte de lo que destaparon las demostraciones queda muy lejos de eso: un contador que bajaba de cero en un descompresor y provocaba una escritura fuera de límites, pero solo con entradas de unos 20 MB con una disposición rara; 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; y el redescubrimiento de CVE-2026-56132 en libexpat. Una demostración destapó además un bug lógico que nunca provoca un fallo: una función para limitar qué archivos puede cargar una aplicación no siempre se aplicaba. La idea de los autores: el simple intento de demostrar encuentra bugs reales, se complete o no.

Dónde se acaba «demostrado»

El artículo es claro en esto, y creo que es su parte más útil. «Verificado formalmente» no significa «sin bugs». Significa que el código cumple las reglas que se escribieron, en la máquina que se modeló. Nombra dos huecos:

• La máquina. Las pruebas tratan de binarios RISC-V estáticos, de un solo hilo, enlazados con musl. Casi todo el mundo ejecuta estas bibliotecas en x86 o ARM, enlazadas dinámicamente con glibc.
• El enunciado. AddressSanitizer no detecta todos los bugs de memoria, no se verificaron todos los puntos de entrada y quien llama a la biblioteca todavía puede usarla mal.

Qué significa para un equipo normal

Seguramente no vas a escribir Rocq pronto. Pero el método parte de algo que muchos equipos ya tienen: un test que expresa una propiedad. Un harness de fuzzing que falla cuando una ida y vuelta no cuadra es una especificación disfrazada, y el artículo señala que demostrar que ese test nunca falla equivale a demostrar la propiedad misma. Un pequeño ejemplo de la forma, ilustrativo y con nombres de función de ejemplo:

#include <assert.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>

/* your library's own functions; the names are placeholders */
size_t encode(const uint8_t *in, size_t n, uint8_t **out);
size_t decode(const uint8_t *in, size_t n, uint8_t **out);

int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size) {
  uint8_t *packed = NULL, *back = NULL;
  size_t packed_n = encode(data, size, &packed);
  size_t back_n = decode(packed, packed_n, &back);
  assert(back_n == size && (size == 0 || memcmp(back, data, size) == 0));
  free(packed);
  free(back);
  return 0;
}

Escribir tests así, donde un fallo significa que se rompió una regla enunciada, sirve hoy mismo con un fuzzer normal, y es justo lo que este tipo de herramienta podrá convertir más adelante en una demostración. Theorem dice que ofrece ejecutar el mismo proceso para otros proyectos de código abierto y que publica una skill de Claude para ayudar a los desarrolladores a empezar a verificar su propio código.

Siguiente paso: elige un parser o un codificador de tu código y escribe la propiedad que siempre debe cumplir como un test que falle de forma visible. Después lee la sección de limitaciones del artículo original antes de fiarte de cualquier etiqueta de «verificado formalmente». Fuente: Anthropic Frontier Red Team, LLMs are making formal software verification feasible at a much larger scale.