Tim Verifikasi Formal kami yang dipimpin oleh @PetarMax, dengan dukungan dari @EthereumFndn, telah memverifikasi di Lean kebenaran ekstensi OpenVM RISC-V yang dibuat oleh @axiom_xyz. Pekerjaan ini membuktikan kebenaran tingkat instruksi dan, untuk pertama kalinya, eksekusi dan konsistensi memori. 🧵