CertiK afirma que ha terminado la verificación formal de zkWasm, una máquina virtual de conocimiento cero para programas WebAssembly, con demostraciones comprobadas por máquina escritas en el asistente de demostraciones Coq. La compañía anunció el resultado el 28 de septiembre, aunque el proyecto no es nuevo. Su serie de publicaciones técnicas sobre el trabajo se remonta a abril de 2024, cuando CertiK describió por primera vez una verificación completa de los circuitos de zkWasm.
zkWasm permite a un desarrollador demostrar que un programa WebAssembly se ejecutó correctamente sin revelar el cálculo. El proyecto de código abierto proviene de Delphinus Lab. Todo lo que se construye sobre él confía en los circuitos, los sistemas de restricciones que deciden qué cuenta como una ejecución válida. Si se omite una restricción, un probador deshonesto puede conseguir que se acepte una ejecución falsa, socavando silenciosamente toda demostración que dependa de ella. CertiK, que afirma haber trabajado con más de 5.500 clientes empresariales, presenta la verificación formal como un paso más allá de las auditorías y las pruebas. En la práctica, eso significa que un verificador de demostraciones confirma que el código cumple una especificación matemática para cada entrada, no solo las que alguien pensó en probar.
Lo que CertiK afirma haber demostrado
Según el comunicado, las demostraciones establecen dos propiedades. La primera es la solidez: cada traza de ejecución aceptada corresponde a una ejecución válida del programa Wasm. La segunda, que CertiK denomina solidez del conocimiento, es que un probador no puede producir una demostración válida para una ejecución incorrecta. El trabajo cubre operaciones aritméticas y a nivel de bits, el acceso a memoria, el flujo de control y las llamadas a funciones. En 2024, CertiK calificó el proyecto como la primera verificación formal completa de una zkVM del mundo. El nuevo comunicado lo sitúa entre los esfuerzos más completos realizados hasta ahora sobre una zkVM en producción.
El método consistió en traducir la lógica de los circuitos Halo2 de zkWasm a Coq y demostrar afirmaciones sobre la traducción. El README público de CertiK indica que la traducción se hizo a mano y se mantuvo cercana al código fuente de Rust para limitar los errores. El desarrollo interno abarca unas 33.000 líneas de Coq, de las cuales unas 21.000 son demostraciones. (El proyecto Coq ha pasado a llamarse Rocq desde 2025, aunque los materiales de CertiK siguen usando el nombre antiguo.)
El comunicado señala que surgieron sutiles problemas de corrección que se resolvieron, sin contarlos ni calificarlos. El sitio de CertiK es más específico. Enumera dos fallos de solidez en zkWasm: una restricción ausente en una carga de memoria, detectada en revisión manual, y restricciones ausentes en la instrucción Return que permitían retornos falsos, detectadas por las demostraciones. Cualquiera de los dos, afirma CertiK, podría permitir que un probador malicioso hiciera pasar una demostración no válida ante el verificador.
Otros equipos también están verificando las zkVM
CertiK no está solo en esto. La Ethereum Foundation dirige un proyecto de verificación formal de zkEVM dotado con 20 millones de dólares. Uno de sus investigadores señaló en el resumen de un taller de 2026 que el impulso por verificar las partes centrales de las zkVM para la capa base de Ethereum lleva más de un año en marcha, con muchos equipos implicados. Certora ganó una subvención de la fundación en febrero para verificar las autoprecompilaciones, una optimización de circuitos. Nethermind, trabajando en Lean en lugar de Coq, creó herramientas que incorporan las restricciones de Halo2 a un asistente de demostraciones y las utilizó para encontrar un fallo crítico en un circuito Keccak-256 de Scroll. Ese circuito ya había quedado obsoleto, y Nethermind afirmó que el fallo no habría podido explotarse porque el probador de Scroll está centralizado.
Lo que las demostraciones no cubren
El propio README de CertiK expone los límites. El objetivo es demostrar que los circuitos son sólidos con respecto a la semántica de WebAssembly, y todo lo que queda fuera de los circuitos Halo2 está fuera del alcance. Eso incluye el código Rust que construye las tablas, el intérprete Wasmi y el propio Halo2. La instrucción de llamada externa se omite porque no tiene restricciones reales. La lógica de decodificación de instrucciones se auditó a mano en lugar de demostrarse, y parte del Rust que genera restricciones se asume correcto. Así, la garantía cubre los circuitos, mientras que el resto se acepta por confianza.
Los observadores externos aún no pueden comprobarlo todo. El repositorio público de GitHub publica las definiciones y los enunciados de los teoremas, de modo que los lectores pueden ver qué se afirmó, pero sustituye las demostraciones por marcadores de posición. El anuncio no dice si se publicarán, qué versión de zkWasm se verificó ni qué cambió desde 2024. Cualquier garantía sobre las demostraciones depende además de que Halo2 haga su trabajo, y el README sitúa a Halo2 fuera del alcance verificado.
