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.
π₯· Pretty-printing of Rust ZK constraints
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.
π₯· Formal verification of an OpenVM chip
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.
π¦ What to verify in a zkVM
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.
π¦ Short introduction to Rocq
In this blog post, we present a short introduction to Rocq, a formal verification system, as a summary of the guide Rocq in a Hurry from Yves Bertot of the Rocq team.
Rocq is the formal system that we use exclusively, but other interactive theorem provers work the same way. From this introduction, you can get a sense of how the verification of mathematical statements or security properties of programs works.
π₯· Formal verification of LLZK circuits in Rocq
π₯· Semantics for LLZK in Rocq
LLZK is a language designed to implement zero-knowledge circuits. We wrote a translation tool from this language to a representation in the formal language Rocq.
In this blog post, we present how we give a semantics to all the primitive operations of LLZK in Rocq. The end-goal is to provide a way to formally verify that a zero-knowledge circuit is safe, that is to say, without under-constraints.
π₯· Beginning of a formal verification tool for LLZK
Here we present the beginning of our work to develop a formal verification tool for LLZK from Veridise, a new language designed to implement zero-knowledge circuits. The zero-knowledge technology is how future versions of Ethereum are planned to be implemented.
As usual, our technique is to work by translation to the Rocq formal verification language, using a representation as similar as possible to the source code to simplify reasoning. Then, we will be able to verify that:
- For any possible inputs, a circuit correctly computes a functional specification (no over-constraint).
- There are no possible invalid witnesses that can be accepted by the circuit (no under-constraint).
π¦ Functional specification of the ADD instruction of the EVM
In this blog post, we present how we specify and verify the implementation of the ADD instruction of the EVM virtual machine in Rust.
We give a functional specification, meaning that we show the implementation to be equivalent to an idealized version written in the Rocq language. As the Rust code for this instruction involves rather advanced features of Rust, the same techniques could apply to verify a large set of Rust programs.
π¦ Beginning of translation of OpenVM to Rocq
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.