El ingeniero y criptógrafo conocido como imperialviolet —figura vinculada al proyecto de navegador Chromium de Google— ha presentado esta semana un experimento singular: un descompresor completo del algoritmo Zstandard (zstd) implementado y verificado formalmente en el lenguaje de programación dependiente Lean, con asistencia de un modelo de lenguaje de gran tamaño (LLM) para la automatización de pruebas. El trabajo, publicado el 26 de julio de 2026 en su blog personal (www.imperialviolet.org), ilustra de manera práctica una hipótesis que el campo de la verificación formal llevaba años explorando: que los LLM podrían reducir drásticamente el coste asociado a demostrar teoremas en sistemas de tipos dependientes.
Lean, junto con Coq (recientemente renombrado Rocq), pertenece a la familia de lenguajes con tipos dependientes, capaces de codificar y enforcing invariantes arbitrariamente sutiles directamente en el sistema de tipos. La promesa es atractiva: en lugar de depender de comentarios que se desactualizan o de convenciones que se diluyen con el crecimiento del equipo, los invariantes quedan formalizados y verificados por una máquina. El problema histórico, según explica el autor, ha sido el esfuerzo de demostración. Citando el caso retrospectivo del microkernel seL4 —publicado por Trustworthy Systems—, recuerda que aquel proyecto, pese a contar con ingenieros altamente experimentados, invirtió aproximadamente diez veces más tiempo en la prueba formal que en el diseño e implementación del código, generando más de veinte veces más líneas de prueba que de C.
Históricamente, la automatización se ha encomendado a solvers SMT, como en el lenguaje F*. Aunque funcionan para casos sencillos, imperialviolet advierte que es fácil construir entradas que envían al solver a explorar durante horas sin garantía de terminación. Los usuarios avanzados desarrollan, según su experiencia, una intuición casi mística sobre qué formulación satisfará al motor. La novedad es que, gracias a los LLM y a un principio conocido como irrelevancia de la prueba —según el cual, una vez que el enunciado es correcto, el contenido concreto de la demostración importa menos que su mera existencia—, esa automatización podría ser ahora mucho más capaz.
El banco de pruebas elegido fue Zstandard, el algoritmo de compresión desarrollado por Yann Collet que, sobre la base del trabajo seminal de Jarek Duda sobre Asymmetric Numeral Systems (ANS), cuenta con un RFC oficial (RFC 8878) y se perfila como el heredero práctico de gzip. El autor destaca que Zstandard emplea codificación Huffman y, en su nivel de mayor compresión, FSE (Finite State Entropy), una máquina de estados que reparte un número de estados proporcional a la probabilidad de cada símbolo y cuya lectura promedio de bits por símbolo puede aproximarse a la entropía teórica sin limitarse a números enteros.
El artículo, no obstante, queda interrumpido en plena explicación de la tabla de estados de FSE, por lo que los detalles finales sobre el grado de automatización obtenido, el tamaño del código de prueba generado y las métricas comparativas entre el descompresor verificado y la implementación de referencia no han podido corroborarse a partir de la fuente facilitada. Esta ausencia de conclusiones explícitas sobre el rendimiento de la combinación Lean+LLM en este experimento concreto constituye una limitación a la hora de evaluar el alcance real del anuncio.
En conjunto, el trabajo se inscribe en una línea creciente de investigación que explora cómo los LLM pueden integrarse con demostradores interactivos de teoremas. Si los resultados fueran positivos a gran escala, la implicación sería significativa: la verificación formal, durante mucho tiempo considerada un lujo reservado a sistemas críticos como microkernels o criptografía de aviónica, podría convertirse en una herramienta cotidiana de ingeniería de software. Por ahora, el experimento de imperialviolet debe leerse como una prueba de concepto temprana y estimulante, pero todavía sin métricas publicadas que permitan calibrar su verdadero impacto.