5 posts tagged with "zkVM"

In this blog post, we present our work to formally verify the determinism of the Keccak precompile ZK circuits in Plonky3 using our 🍀 Garden framework.

Concretely, this means that:

• This complex circuit is safe for use with all the zkVMs based on Plonky3.
• The 🍀 Garden framework is very expressive and can verify arbitrary circuits, as optimized precompiles are one of the most complex ZK circuits.

The formal verification of the determinism of ZK circuits is important, as this is one of the main sources of critical bugs in zkVMs, and these bugs cannot be found by other means, like testing, while most of the unverified zkVMs have at least one such bug.

In our previous blog post 🥷 Formal verification of an OpenVM chip, we have seen how to verify the determinism of the branch_eq chip of OpenVM. Now, we will see how to verify its completeness, meaning that it always accepts a valid witness for any possible input.

Many zkVMs are implemented in Rust, using the Plonky3 library to describe their circuits. While Rust is efficient and expressive for describing complex circuits, it is a complex language when it comes to formal verification. We present here a way to pretty-print the list of constraints generated by a Plonky3 program. That way, we will be able to import the constraints in a formal verification system like Rocq to make sure they are safe and correct.

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.