Nuestro equipo de Verificación Formal, liderado por @PetarMax, con el apoyo de @EthereumFndn, ha verificado en Lean la corrección de la extensión RISC-V de OpenVM desarrollada por @axiom_xyz. Este trabajo demuestra la corrección a nivel de instrucción y, por primera vez, la ejecución y la consistencia de la memoria. 🧵