Il nostro team di Verifica Formale, guidato da @PetarMax, con il supporto di @EthereumFndn, ha verificato in Lean la correttezza dell'estensione OpenVM RISC-V costruita da @axiom_xyz. Questo lavoro dimostra la correttezza a livello di istruzione e, per la prima volta, la coerenza dell'esecuzione e della memoria. 🧵