Nossa equipe de Verificação Formal, liderada por @PetarMax, com o apoio da @EthereumFndn, verificou em Lean a correção da extensão OpenVM RISC-V construída pela @axiom_xyz. Este trabalho comprova a correção em nível de instrução e, pela primeira vez, a execução e a consistência da memória. 🧵