6 posts tagged with "zero-knowledge"

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.

In this blog post, we present a short example about how we define reasoning rules in Rocq to formally verify the safety of zero-knowledge circuits written in LLZK.

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.

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).

In this post, we present the beginning of our work to translate programs written in the Circom circuit language to the 🐓 Coq proof assistant. This work is part of our research on the formal verification of zero-knowledge systems.

We will aim to write more regularly about what we are doing, even if the posts are then shorter. Here, we focus on the translation part for a simple example without defining a semantics for the generated Coq code.