LLMs automatizan pruebas formales en Lean para verificar zstd

El equipo detrás de seL4, el microkernel formalmente verificado, documentó algo brutal en su retrospectiva: escribir las pruebas formales les tomó unas 10 veces más tiempo que diseñar e implementar el sistema, y terminaron con más de 20 líneas de prueba por cada línea de C. Ese costo explica por qué lenguajes de tipos dependientes como Lean o Coq (rebautizado recientemente como Rocq) quedaron reservados a proyectos con presupuesto casi ilimitado.

Un ingeniero que trabaja en criptografía en Google y escribe el blog ImperialViolet decidió probar si los modelos de lenguaje bajan ese costo. Construyó, de punta a punta, un descompresor de Zstandard en Lean, con las pruebas generadas por un LLM en vez de a mano.

TL;DR

• El proyecto seL4 documentó que verificarlo formalmente tomó 10 veces más tiempo que diseñarlo y programarlo.
• El código de prueba de seL4 terminó siendo más de 20 veces más extenso que su código C.
• Un ingeniero de ImperialViolet implementó un descompresor completo de Zstandard en Lean con pruebas generadas por un LLM.
• Zstandard, creado por Yann Collet, usa la codificación de entropía ANS de Jarek Duda en vez del Huffman de gzip.
• F* delega las pruebas a un solver SMT que a veces tarda horas sin converger en casos complejos.
• La proof irrelevance permite que, una vez que un teorema type-checea, el contenido de la prueba deje de importar.
• Coq cambió de nombre a Rocq, un dato mencionado de pasada en el post original del experimento.
• Zstandard tiene su especificación formal en la RFC 8878, usada como referencia para construir el decodificador.

Qué pasó

El autor de ImperialViolet publicó el experimento el 26 de julio de 2026: implementó un decodificador completo del formato Zstandard (zstd) en Lean, delegando la generación de las pruebas formales a un LLM. El objetivo no era solo tener un decodificador que funcione, sino que el type-checker de Lean certificara matemáticamente que ciertas propiedades del código, por ejemplo que nunca se lea fuera de los límites de un buffer, se cumplen siempre, sin depender de tests.

La elección de Zstandard no es casual. Es el compresor creado por Yann Collet que se apoya en la codificación de entropía ANS (Asymmetric Numeral Systems) desarrollada por Jarek Duda, y viene desplazando a gzip como estándar de facto en distribuciones Linux, formatos de contenedor y protocolos de red. Tiene una especificación en la RFC 8878, densa pero completa, que el autor usó como referencia línea por línea para escribir el decodificador.

Contexto e historia: el problema de siempre con los tipos dependientes

Los lenguajes de tipos dependientes permiten expresar invariantes en el propio sistema de tipos: no solo "esta función recibe un array", sino "esta función recibe un array de exactamente N elementos donde N es par". En teoría, eso convierte errores que hoy se descubren en producción en errores de compilación. En la práctica, escribir esas pruebas a mano es carísimo.

El caso de referencia es seL4, el microkernel verificado formalmente en Isabelle/HOL. Su retrospectiva se cita una y otra vez en la comunidad porque cuantifica el problema: pese a que el equipo desarrolló experiencia considerable, gastó cerca de 10 veces más tiempo probando que diseñando e implementando, y terminó con más de 20 veces más líneas de prueba que de código C. Ese ratio es el que vuelve inviable aplicar verificación formal a la mayoría del software.

Para bajar ese costo surgió F*, un lenguaje que delega buena parte de la carga a un solver SMT (Satisfiability Modulo Theories), que intenta demostrar automáticamente cada obligación. Funciona bien en casos simples, pero es fácil escribir una prueba que hace que el solver se cuelgue durante horas sin converger. Quien usa F* con frecuencia termina desarrollando intuición sobre qué formulaciones "le gustan" al solver, una forma de superstición técnica más que de ingeniería predecible.

⚠️ Ojo: delegar pruebas a un solver SMT no elimina el costo, lo traslada. En vez de escribir la prueba a mano, hay que aprender a formular el problema de un modo que el solver pueda resolver en tiempo razonable, y eso no siempre es más barato.

Hay un detalle técnico que hace prometedora la combinación con LLMs: la proof irrelevance (irrelevancia de la prueba). Una vez que un enunciado se demuestra correcto, el contenido concreto de esa prueba deja de importar: solo importa que exista. Esto no es absoluto, hay dos matices. Primero, lo que el equipo de seL4 llamó "ingeniería de pruebas": estructurar las demostraciones para que, cuando el código cambie, no haya que rehacerlas desde cero. Segundo, una prueba suficientemente enredada puede hacer que el propio type-checker consuma cantidades enormes de memoria y tiempo, incluso si es correcta.

Por qué Zstandard es un buen banco de pruebas

Zstandard es, como gzip y bzip2, un compresor de la familia LZ77: reemplaza secuencias repetidas por referencias a apariciones anteriores. La diferencia está en la codificación de entropía que usa después de esa etapa. Gzip usa Huffman; Zstandard usa ANS, que logra una compresión más ajustada a costa de un diseño más intrincado. Esa complejidad adicional es justo lo que hace interesante intentar verificarlo formalmente: hay más superficie donde un desajuste entre la especificación y la implementación puede esconder un bug.

zstd y gzip quedan en su propia categoría de velocidad frente a bzip2 y lzma.

El propio autor midió, sobre 64 MiB del código fuente de Lean/mathlib, la relación entre espacio ahorrado y velocidad de descompresión de los cuatro compresores más usados. La tabla resume las diferencias cualitativas que documentó:

CompresorFamilia de algoritmoFortalezaLimitación

zstdLZ77 + ANSDescompresión muy rápida manteniendo buena relación de compresiónNo alcanza el ratio máximo de lzma en corpora grandes
gzipLZ77 + Huffman (DEFLATE)Ubicuo, con implementaciones muy optimizadas (por ejemplo, la de Apple)Peor ratio de compresión que zstd o lzma
bzip2Burrows-Wheeler TransformBuen ratio en texto altamente repetitivoDescompresión sensiblemente más lenta que zstd
lzma (XZ/LZMA2)LZ77 + modelado de rangoLa mejor compresión del grupoLa más lenta para descomprimir

El propio autor advierte que sus mediciones vienen de la máquina que estaba usando en ese momento (una Mac), y que en esa plataforma gzip está especialmente optimizado, así que los números absolutos no son comparables entre equipos distintos. Lo reproducible es el orden de magnitud: en escala logarítmica, zstd y gzip quedan en su propia categoría de velocidad frente a bzip2 y lzma.

Pruebas formales con ayuda de un LLM: cómo funciona el ciclo

La mecánica es más simple de lo que suena. Se escribe el enunciado del teorema en Lean, por ejemplo "el índice de lectura del buffer nunca supera su tamaño". Un LLM propone un script de tácticas que, en teoría, demuestra ese enunciado. El type-checker de Lean lo evalúa: si compila, la prueba queda aceptada para siempre, sin importar lo torpe o larga que sea. Si falla, el error se le devuelve al modelo junto con el mensaje exacto del compilador, y se repite el ciclo.

flowchart TD
    A["Enunciado del teorema en Lean"] --> B["El LLM propone un script de tacticas"]
    B --> C["El type-checker de Lean evalua la prueba"]
    C -->|"Error de tipos"| D["El LLM recibe el mensaje de error"]
    D --> B
    C -->|"Compila"| E["Prueba aceptada: el contenido ya no importa"]

Este ciclo funciona gracias a la proof irrelevance mencionada antes: no hace falta que la prueba sea elegante ni corta, solo que exista. Es la misma razón por la que un humano puede escribir una demostración fea y el compilador la acepta igual. La diferencia con F* es que acá no hay un solver genérico tratando de adivinar la estrategia: el LLM ya conoce patrones idiomáticos de Lean (inducción, simp, análisis de casos) porque los vio en su entrenamiento, y los aplica de forma más dirigida que una búsqueda ciega.

Un ejemplo mínimo, del estilo que cualquiera puede probar apenas instala Lean, ilustra la sintaxis:

theorem suma_conmutativa (a b : Nat) : a + b = b + a := by
  induction a with
  | zero => simp
  | succ n ih => simp [Nat.succ_add, ih]

Ese teorema es trivial, pero el patrón escala. En un decodificador de compresión, el tipo de invariante que interesa es distinto: que un puntero de lectura nunca se salga del buffer. En Lean eso se puede modelar con Fin, un tipo que representa "un número natural menor que N" directamente en su definición:

structure VentanaDescompresion where
  datos : Array UInt8
  pos   : Fin datos.size

def siguienteByte (v : VentanaDescompresion) : UInt8 :=
  v.datos.get v.pos

Con pos : Fin datos.size, es imposible construir una VentanaDescompresion con un puntero fuera de rango: el propio tipo lo prohíbe. siguienteByte no necesita ningún chequeo en tiempo de ejecución ni puede fallar por un acceso inválido, porque el compilador ya descartó esa posibilidad antes de generar el binario. Ese es exactamente el tipo de error, lectura fuera de límites en un decodificador de compresión, que generó vulnerabilidades reales en librerías como zlib a lo largo de los años.

💡 Tip: la proof irrelevance es lo que hace viable delegarle la prueba a un LLM. Como el contenido de la demostración no afecta el binario final, no importa si el modelo tarda 40 intentos en encontrar el script correcto: solo importa el resultado.

Cómo empezar: instalar Lean y compilar tu primera prueba

Lean 4 se instala con elan, su gestor de versiones (el equivalente a lo que rustup es para Rust). Los comandos cambian según el sistema operativo:

# macOS / Linux
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# Windows (PowerShell)
irm https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 | iex

Con elan instalado, se crea un proyecto nuevo con Lake, el gestor de builds de Lean, y se compila:

lake new mi_prueba math
cd mi_prueba
lake build
lake env lean --version

Si lake env lean --version devuelve un número de versión sin errores, el entorno quedó operativo. A partir de ahí, pegar el ejemplo de suma_conmutativa de más arriba en un archivo .lean y correr lake build es la forma más rápida de comprobar que el type-checker realmente rechaza pruebas incorrectas: basta con borrar una línea del script de tácticas para ver el error.

Para experimentar con LLMs integrados al flujo de pruebas sin escribir la infraestructura desde cero, dos proyectos open source sirven de punto de partida: LeanDojo, que expone el estado de las pruebas de Lean como un entorno consultable por un modelo, y LeanCopilot, que integra sugerencias de tácticas generadas por modelos directamente en el editor.

Impacto y análisis

El resultado concreto, un decodificador de Zstandard que funciona y que Lean certificó según ciertas propiedades, importa menos que la pregunta que responde: si la proof irrelevance vuelve indiferente qué tan fea es una prueba, entonces el costo que antes pagaban ingenieros humanos (redactar y depurar cada demostración) es exactamente el tipo de tarea repetitiva, con feedback inmediato del compilador, que un LLM puede iterar miles de veces sin fatiga.

Eso no resuelve los dos matices que ya complicaban la proof irrelevance antes de que existieran los LLMs. La ingeniería de pruebas, estructurarlas para que sobrevivan a cambios de código, sigue siendo un problema de diseño: un LLM puede regenerar la prueba entera cada vez que el código cambia, pero eso puede volverse costoso si el proyecto crece. Y una prueba que hace explotar el type-checker en memoria sigue siendo un problema, la genere quien la genere.

El type-checker de Lean acepta o rechaza la prueba sin ambigüedad, sin importar su origen.

Hay además un riesgo de reemplazar un tipo de misticismo por otro. Con F*, la comunidad desarrolló intuición sobre qué formulaciones el solver SMT podía resolver. Con LLMs generando pruebas en Lean existe un riesgo parecido: que el proceso funcione mejor con ciertos estilos de enunciado y peor con otros, sin que quede claro por qué, simplemente porque coincide con patrones vistos en el entrenamiento del modelo.

Qué sigue

El propio autor de ImperialViolet enmarca esto como una prueba de concepto, no como un producto listo para usar en librerías de compresión en producción. El paso lógico siguiente es replicar el experimento en código con historial real de vulnerabilidades, como parsers de formatos binarios o implementaciones de protocolos de red, para medir si el enfoque escala más allá de un decodificador escrito para probar la idea.

El cuello de botella que queda por resolver no es generar la prueba una vez, sino mantenerla viva cuando el código cambia semana a semana. Si un LLM puede regenerar la prueba completa a un costo marginal bajo cada vez que hay un commit, la ingeniería de pruebas que le costó tanto tiempo a seL4 podría dejar de ser un problema exclusivamente humano. Esa es la apuesta implícita detrás del experimento.

📖 Resumen en Telegram: Ver resumen

Probalo vos: instalá elan con el comando de arriba, pegá el teorema de suma_conmutativa en un archivo .lean y corré lake build para ver el type-checker de Lean en acción en menos de cinco minutos.

Preguntas frecuentes

¿Qué es un lenguaje de tipos dependientes?

Es un lenguaje donde los tipos pueden depender de valores, no solo de otros tipos. Eso permite expresar invariantes como "un array de exactamente N elementos" o "un índice siempre menor que el tamaño del buffer" directamente en la firma de una función, y que el compilador los verifique.

¿Por qué Coq cambió de nombre a Rocq?

El nombre generaba confusión y bromas recurrentes en un contexto de habla inglesa. El proyecto adoptó Rocq como nuevo nombre, aunque la base técnica del lenguaje se mantiene.

¿Qué significa "proof irrelevance"?

Es la propiedad por la cual, una vez que un teorema type-checea correctamente, el contenido específico de esa demostración deja de tener relevancia para el programa: solo importa que la prueba exista y sea válida, no cómo esté escrita.

¿Por qué seL4 tardó tanto en verificarse formalmente?

Porque escribir pruebas manuales para cada propiedad del microkernel resultó mucho más laborioso que escribir el código original: el equipo reportó cerca de 10 veces más tiempo dedicado a probar que a diseñar e implementar, con más de 20 veces más líneas de prueba que de código C.

¿Este enfoque ya se puede usar en producción?

No como una solución empaquetada. El experimento de ImperialViolet es una prueba de concepto sobre un decodificador de Zstandard, no una librería lista para reemplazar implementaciones existentes en sistemas críticos.

¿En qué se diferencia de F*?

F* delega las pruebas a un solver SMT genérico, que puede colgarse buscando una demostración sin garantía de encontrarla a tiempo. El enfoque con LLMs en Lean usa un modelo entrenado en patrones idiomáticos del lenguaje, que itera sobre los errores del type-checker en vez de depender de un solver de propósito general.

Referencias

• ImperialViolet, "We have proof automation now": el post original que documenta el experimento de Zstandard en Lean.
• RFC 8878: la especificación oficial del formato de compresión Zstandard.
• sel4.systems: sitio oficial del microkernel seL4 y su retrospectiva de verificación formal.
• leanprover.github.io: documentación oficial del lenguaje Lean 4.
• github.com/lean-dojo/LeanDojo: entorno open source para conectar LLMs con el probador de teoremas de Lean.

📱 ¿Te gusta este contenido? Únete a nuestro canal de Telegram @programacion donde publicamos a diario lo más relevante de tecnología, IA y desarrollo. Resúmenes rápidos, contenido fresco todos los días.