Here, we present our beginning work of translating part of the OpenVM code to the proof assistant 
Rocq. The aim is to experiment around the formal verification of the zero-knowledge circuits of this zkVM based on the Plonky3 library. One of the aims of the zkVMs is to increase the scalability of the blockchains by packing many transactions in a single zk proof.
🦀 Beginning of translation of OpenVM to Rocq
· 8 min read