«FlashProve»: la criptografía que demuestra qué modelo te respondió

Hoy no hay forma de saber con certeza qué modelo generó una respuesta de IA. Si consumes un modelo a través de un intermediario que enruta peticiones, ese intermediario podría servirte uno más barato y tú nunca te enterarías. Si alguien compromete el servidor de inferencia, puede alterar el flujo de tokens, devolverte malware en lugar de una respuesta o, en un escenario más sutil, dejar que un modelo se sustituya a otro para esquivar los controles que se aplican al modelo más potente. El resultado de una conversación no lleva firma, y una firma es exactamente lo que falta.

El 2 de noviembre, Anthropic publicó un avance que ataca el problema de frente: FlashProve, un prototipo de código abierto de inferencia demostrable. La idea es sencilla de enunciar y muy difícil de conseguir: cada respuesta va acompañada de una prueba criptográfica de que la han generado los pesos concretos del modelo que el proveedor dice estar sirviendo, sin revelar ni un bit de esos pesos. No es una metáfora. Hay un repositorio, un informe técnico, un verificador escrito en C++, otro verificador escrito en el asistente de pruebas Lean y tablas de tiempos medidas al detalle.

Qué es una prueba de inferencia

La técnica que hay debajo es una zkSNARK, un argumento criptográfico usado desde hace años en las redes de segunda capa de Ethereum (Starknet, Mantle) para demostrar que una transacción se ha calculado bien sin revelar quién la ha firmado ni los datos que la sostienen.

Sus propiedades son las que hacen útil la idea:

• Completitud. Si la afirmación es cierta, la prueba se acepta.
• Solidez. Una prueba falsa se rechaza, salvo con una probabilidad despreciable.
• Conocimiento cero. La prueba no filtra información sobre los pesos del modelo.
• Suficiencia. Comprobar la prueba es mucho más barato que rehacer la inferencia: unas horas de GPU se convierten en segundos de CPU.

El paralelismo útil es el del notario. Un notario no te enseña el contrato original ni te explica cómo lo redactó; te entrega un sello que certifica que aquel documento con aquel texto es el que se firmó. FlashProve automatiza ese sello para respuestas de IA.

Cómo funciona: un compromiso y una prueba

El sistema tiene dos fases.

La fase offline ocurre una vez por modelo. El proveedor calcula un compromiso sobre los pesos: una huella corta que fija una y sola elección de pesos, mientras los pesos en sí siguen ocultos. En la implementación publicada, ese compromiso tarda unos 39 minutos en generarse y ocupa alrededor de 6,5 MB; el cliente lo descarga una vez y el proveedor guarda unos 2,15 GB de material por compromiso. El compromiso caduca: el proyecto calcula unos 16 millones de peticiones por compromiso, y cada tabla de mensajes sirve 688.127 lotes, así que pasado ese punto hay que volver a comprometer el modelo.

La fase online ocurre por petición. Cuando llegan 24 peticiones, el demostrador produce una prueba por respuesta que afirma, en términos lógicos, que el modelo comprometido genera esos tokens concretos con esa entrada. Cada prueba ocupa 18,78 MB y tarda unos segundos en comprobarse con un procesador normal, sin GPU: 17 segundos con 24 hilos y 21 con uno solo.

Dos detalles de diseño explican por qué el sistema es viable:

• El trabajo se paga por experto, no por parámetro. En una arquitectura Mixture-of-Experts, cada token activa un subconjunto pequeño de las redes expertas. En Llama 4 Maverick, de unos 400.000 millones de parámetros totales, se usan alrededor de 17.000 millones por token. El demostrador trabaja en proporción a los expertos que realmente se activaron, aunque la prueba siga ocultando cuáles fueron.
• Las peticiones se demuestran por lotes y a posteriori. El motor de inferencia termina el texto y después el demostrador recorre los lotes terminados en una sola pasada, abriendo el compromiso una vez por lote en lugar de una vez por petición.

Las cifras: cuánto ha avanzado esto

El punto de partida importa, porque la idea llevaba años siendo una curiosidad de laboratorio. En 2024, zkLLM demostraba LLaMA-2 de 13.000 millones: unos 15 minutos de GPU para 2.048 tokens de entrada, del orden de 0,001 tokens por segundo token a token, o unos 2,5 por segundo en lote. En 2025, zkGPT bajó GPT-2 a 21,8 segundos por token y zkPyTorch demostró Llama-3 de 8.000 millones a unos 150 segundos por token. VerInf, el único trabajo previo que había demostrado el mismo modelo que usa Anthropic, reportaba 14,3 horas para 1.000 tokens y una prueba de 93,6 MB que tardaba casi un día en verificarse.

FlashProve demuestra Llama 4 Maverick, con 400.000 millones de parámetros, unos 17.000 millones activos por token y pesos públicos cuantizados a 4 bits (unos 232 GB), a 110 tokens por segundo en una sola GPU H100, con pruebas de 19 MB que se verifican en segundos. En el desglose fino: 17,4 tokens por segundo con una petición por lote, 76,3 con ocho y 111,2 con 24.

El coste es alto y conviene decirlo sin rodeos: demostrar es entre 70 y 95 veces más lento que la inferencia normal. Anthropic lo midió contra vLLM, un motor de inferencia de uso común, con ocho H100: para procesar el mismo lote de 24 peticiones hacen falta unas 72 veces más GPU, y unas 94 si el motor está al máximo de carga. La memoria tampoco es trivial: unos 290 GB de RAM de host junto a una GPU de 80 GB, y casi 300 GB solo para generar el compromiso.

El salto en tres años es real: de 0,001 tokens por segundo a 110. En términos de coste, la inferencia demostrable es hoy un producto de nicho para auditorías de alto valor, no el modo por defecto de servir inferencia.

El ángulo de seguridad: qué atrapa

El valor para un equipo de seguridad está en la lista de amenazas que el sistema permite cerrar. Anthropic enumera cuatro desafíos, y el segundo es el que más importa en la práctica.

• Detección de manipulaciones. Un atacante que compromete el servidor de inferencia puede robar los pesos, devolver respuestas maliciosas camufladas entre las legítimas o, en el futuro, ejecutar un modelo distinto del autorizado. Con una zkSNARK atada al compromiso, el atacante tendría que producir pruebas válidas de los pesos esperados, y no puede.
• Procedencia del texto. Aquí hay un caso muy concreto para el sector: una prueba de fracaso. Un proveedor podría adjuntar al parche la constancia de que el modelo de frontera gastó al menos X tokens en un modelo concreto y no encontró ningún fallo. Sin eso, la afirmación «lo escaneamos con un modelo frontera» no es verificable; con eso, es una afirmación con respaldo criptográfico.
• Modelos aprobados. Si la normativa exige servir solo modelos aprobados, el regulador puede pedir la prueba en cada respuesta y comprobar que el compromiso corresponde al modelo autorizado.
• Ritmo de desarrollo. Un regulador que quiera verificar que el hardware del proveedor se dedica a inferencia y no a entrenar un modelo más potente puede pedir los certificados del periodo. La propia Anthropic matiza el límite: la prueba no demuestra que el hardware no esté entrenando por el margen.

El punto flaco: la confianza no desaparece, se traslada

Aquí conviene bajar el ritmo, porque el repositorio es inusualmente honesto sobre sus límites, y esa honestidad es la parte más útil del ejercicio.

La prueba responde a una pregunta muy concreta: el modelo comprometido produce esta respuesta. No responde: este es el modelo que yo creía estar comprando. Un proveedor puede comprometer cualquier modelo que quiera, incluido uno pequeño o degenerado, y demostrarlo con total honestidad. Por eso la documentación insiste en que el identificador de compromiso se obtenga de una parte de confianza y nunca del servidor que estás comprobando ni de los archivos que acompañan a la prueba. La cadena de confianza no se elimina: se hace explícita y se traslada a un punto concreto, el compromiso, que hay que publicar y repartir antes de tiempo.

Hay un segundo matiz, más técnico y más incómodo: la política de verificación por defecto es permisiva. El verificador devuelve dos tipos de aceptación y ambos salen con código 0, así que hay que leer la última línea. La más fuerte, la coincidencia exacta, casi nunca se cumple con motores reales: de 96 respuestas honestas evaluadas con dos motores de inferencia, ninguna habría pasado esa comprobación. La más laxa, la que el verificador llama WITHIN LIMITS, se cumple en 28 de 32 respuestas en las que se había cambiado un solo token por la segunda opción del modelo. Es decir, en el modo que el proyecto recomienda usar, una respuesta falseada puede pasar el filtro. La recomendación del propio proyecto es clara: si no puedes evaluar esos límites, acepta solo la coincidencia exacta.

A eso se suman tres avisos más:

• Una prueba solo cubre los tokens comprobados. Si una respuesta se corta antes de tiempo, verifica como una respuesta más corta, y la prueba no dice quién la pidió ni cuándo.
• La demostración es sobre el modelo entero en aritmética entera y con decodificación voraz. Una implementación real en coma flotante, o un muestreo de tokens, se desvía. En una medición, el token más probable difirió en el 6,81 % de las posiciones.
• Los bits que imprimen los programas son su propia contabilidad, no un teorema. La cifra probada es la del teorema de Lean: alrededor de 124 bits por consulta de hash, con un suelo del orden de 2^-101. Además, dos ataques publicados contra transformaciones de Fiat-Shamir todavía no se han examinado contra este protocolo, y el informe técnico completo no es público ni ha pasado revisión por pares.

Por qué importa la verificación formal

El código criptográfico es frágil por naturaleza: un error de una línea destruye la garantía. La respuesta de Anthropic es la verificación formal: el protocolo y sus propiedades están especificados en Lean 4, un asistente de pruebas donde el teorema se comprueba máquina a máquina.

Las tres propiedades, completitud, solidez y conocimiento cero, están demostradas en Lean, y hay un visualizador interactivo de los teoremas para que un auditor los lea sin instalar Lean. Además se publica un verificador ejecutable en Lean, que acepta lo mismo que el verificador de C++ pero tarda entre 19 y 39 minutos por prueba y puede consumir 14 GB de memoria; el de C++ tarda unos 21 segundos con un hilo y hasta 3,5 GB.

El reparto es lógico y está bien elegido: para la solidez basta con que el verificador sea correcto, y se puede desconfiar por completo del demostrador; para el conocimiento cero hace falta que el demostrador sea correcto, y eso no se puede probar en Lean porque el demostrador real está escrito en CUDA. El propio Anthropic reconoce que quedan dos huecos: los enunciados formales hay que auditarlos a mano para comprobar que dicen lo que dicen, y el código ejecutable hay que auditarlo para comprobar que coincide con el protocolo demostrado.

Y sí: lo escribió Claude

No es un detalle menor. Anthropic sostiene que Claude produjo las mejoras sobre zkSNARKs, que escribió la especificación del protocolo (el propio repositorio la publica como documento) y que las afirmaciones de seguridad de alto nivel están redactadas en Lean para que un humano pueda auditarlas. Es un cambio de fondo en cómo se construye criptografía: en lugar de una biblioteca de Starknet o de un sistema de pruebas, el punto de partida es un modelo de lenguaje que optimiza y un humano que comprueba.

El repositorio está preparado, además, para que lo monte un agente. Incluye un fichero AGENTS.md con reglas de trabajo (nunca como root, nunca saltarse un error con sudo, informar del código de salida y de la última línea) y una ruta de pruebas numerada con requisitos de memoria, disco y tiempo: desde verificar una prueba de ejemplo en un equipo con 2 GB de RAM hasta el modelo real, que pide 330 GB de RAM, 245 GB de disco y una GPU H100 con CUDA 13.2. La versión publicada es la 0.16.0, con licencia Apache 2.0, y el propio README la describe como un artefacto de investigación que no se mantiene y no acepta contribuciones.

Qué hacer con esto

Si operas modelos o los consumes en entornos donde la respuesta importa (seguridad, auditoría, cumplimiento), hay tres acciones concretas:

• Pregunta por las pruebas. Si un proveedor afirma servir un modelo concreto, pide la prueba y el identificador de compromiso, y comprueba que ese identificador lo publicaste tú o te llegó de una parte de confianza, no del servidor.
• Construye el verificador tú mismo. Es software libre y la comprobación tarda segundos. Compilarlo es el primer paso; confiar en el verificador del proveedor, no.
• Lee la última línea, no el código de salida. Los dos tipos de aceptación comparten código 0 y significan cosas muy distintas.

Para un equipo de seguridad, el cambio de fondo es otro: durante años, auditar un modelo fue una declaración de confianza. Con esto, empieza a ser una prueba.

La lección de fondo

La firma no es el detalle, es el sistema. Lo que FlashProve demuestra es que la verificación criptográfica ya no está reñida con la transparencia: se puede probar que alguien ejecutó un cálculo sin enseñar los datos del cálculo. Aplicado a la inferencia, eso significa que la pregunta sobre qué modelo te respondió deja de ser una cuestión de confianza para pasar a ser una cuestión con respuesta demostrable, siempre que alguien se moleste en comprobar la firma.

El resto son cifras: hoy demuestra a 110 tokens por segundo con un sobrecoste de 70 a 95 veces, solo funciona con arquitecturas de expertos y con un modelo entero, y la comprobación por defecto es más laxa de lo que parece. Son límites conocidos, no fallos de diseño. La infraestructura criptográfica no llega lista: llega con sus listas de límites, sus códigos de salida y su documentación de advertencias, y eso también es una señal de madurez.

Fuentes

• Anthropic — Progress on provable inference for large language models (2 de noviembre de 2026)
• Informe técnico de FlashProve
• Repositorio anthropics/FlashProve, con licencia Apache 2.0
• Teorema de solidez en Lean
• Límites conocidos del sistema
• Mediciones de rendimiento
• Visualizador de los teoremas de Lean
• Anthropic Frontier Safety Roadmap