Наша команда формальной верификации под руководством @PetarMax, с поддержкой от @EthereumFndn, проверила в Lean корректность расширения OpenVM RISC-V, разработанного @axiom_xyz. Эта работа доказывает корректность на уровне инструкций и, впервые, согласованность выполнения и памяти. 🧵