Este artículo describe un flujo de trabajo de verificación formal que toma código criptográfico Rust en producción y genera pruebas de corrección certificadas por el núcleo de Lean 4. La canalización articula tres líneas técnicas recientes en una sola cadena operativa. En primer lugar, herramientas de extracción simbólica como Charon y Aeneas (o Hax, de Cryspen) traducen Rust seguro a código Lean 4 en el mónada Result, preservando la semántica necesaria para la verificación. En segundo lugar, bibliotecas formales como ArkLib (verificación de protocolos SNARK sobre reducciones de oráculo interactivas, con formalizaciones de Sum-Check, FRI y WHIR) y CompPoly (polinomios computacionales y aritmética de cuerpos finitos) aportan las especificaciones matemáticas abstractas contra las que se compara el código. En tercero, los probadores de IA Aristotle (Harmonic AI) y Aleph (Logical Intelligence) cierran obligaciones de prueba; el núcleo de Lean revalida cada salida, por lo que la solidez no depende de la corrección del modelo.
El equipo aplicó este flujo en el marco del zkEVM Verification Project de la Ethereum Foundation a primitivos criptográficos de Plonky3 (plegado FRI, aritmética de los cuerpos Mersenne31 y KoalaBear, evaluación de polinomios por Horner) y de RISC Zero (verificación de inclusión Merkle). Adicionalmente, Aleph demostró dos teoremas sobre cotas en compute_log_arity_for_round de Plonky3 que permanecían como sorry.
Los autores detallan cuatro contribuciones: la propia canalización, su aplicación a ocho dianas críticas para el consenso, un informe empírico de qué obligaciones cerró la IA y cuáles exigieron trabajo manual, y un catálogo de brechas de ingeniería — deriva de la toolchain de Lean 4 entre herramientas, límites de extracción de Aeneas y Hax — junto a dos soluciones prácticas. El objetivo declarado es reducir la barrera de adopción de la verificación formal y orientar el uso eficaz de la IA en este tipo de flujos.