Skip to main content

· 9 min read

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.

· 6 min read

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.

· 6 min read

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.

· 6 min read

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.

· 7 min read

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

· 5 min read
Guillaume Claret

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.

· 10 min read

In this blog post we present how represent a proof of execution for translated 🦀 Rust programs in  Rocq/Coq, to show that it is possible to type the values and resolve the names. Resolving the names amounts to finding the trait instances and an ordering for the function definitions.

We call these proofs of execution "links". They do not contain memory allocation strategies, which can be defined later in a second step called "simulation". From these links we have all the information to extract a typed execution that is equivalent to the translated code from coq-of-rust. The core of the work presented in this article is in the file CoqOfRust/links/M.v on GitHub.