Ons Formele Verificatie team, geleid door @PetarMax, met ondersteuning van @EthereumFndn, heeft in Lean de correctheid van de OpenVM RISC-V extensie, gebouwd door @axiom_xyz, geverifieerd. Dit werk bewijst de correctheid op instructieniveau en, voor het eerst, de uitvoering en geheugenconsistentie. 🧵