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

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.

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.

In this article we show how we re-build the type and naming information of 🦀 Rust code in  Rocq/Coq, the formal verification system we use. A challenge is to be able to represent arbitrary Rust programs, including the standard library of Rust and the whole of Revm, a virtual machine to run EVM programs.

This blog post provides a review of the existing literature on agent-based systems for automated theorem proving, while presenting a general approach to the problem. Additionally, it serves as an informal specification outlining the requirements for a future system we intend to develop.

This is the last article of a series of blog post presenting our formal verification effort in  Rocq/Coq to ensure the correctness of the type-checker of the Move language for Sui.

Here we show how the formal proof works to check that the type-checker is correct on a particular instruction, for any possible initial states. The general idea is to symbolically execute the code step by step on the type-checker side, accumulating properties about the stack assuming the type-checker succeeds, and then to show that the interpreter will produce a stack of the expected type as a result.

We want to write a series of blog posts about our efforts to use LLMs to formally verify code faster with the  Rocq/Coq theorem prover. Here, we present an experiment consisting of writing all that we are doing so that we can document our reasoning and help LLMs to pick up human techniques.

According to many publications about using generative AI to help formal verification, it is almost impossible to find a proof in "one shot". So, one certainly has to interact with the system, maybe by following the human way. Here we aim to document this "human way" of writing proofs.