2 posts tagged with "zkVM"

In this blog post, we present the formal verification of the determinism of the BranchEq circuit of the OpenVM zkVM. This zkVM provides an implementation of RISC-V with Plonky3, and appears to be very fast even on a CPU.

We do our verification work using the formal verification system Rocq, showing the determinism on a model of the code. To see the other properties that can be verified, you can refer to our previous blog post 🦄 What to verify in a zkVM. We will see later how to make sure that the Rocq model corresponds to the actual Rust implementation of the circuit.

We present in this blog post the main properties that need to be formally verified in the circuits of a zkVM to consider it as secure.

The formal verification of zero-knowledge applications is considered a priority by Vitalik Buterin, the founder of Ethereum, among others. The website ethproofs.org lists zkVMs ready to run Ethereum, with formal verification of the code being one of the criteria to appear as 🟩 green.