Nasz zespół ds. formalnej weryfikacji, kierowany przez @PetarMax, z wsparciem od @EthereumFndn, zweryfikował w Lean poprawność rozszerzenia OpenVM RISC-V stworzonego przez @axiom_xyz. Ta praca dowodzi poprawności na poziomie instrukcji oraz, po raz pierwszy, spójności wykonania i pamięci. 🧵