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.

In this blog post, we present a technique with the  Rocq/Coq theorem prover to define mutually recursive functions using a notation. This is sometimes convenient for types defined using a container type, such as types depending on a list of itself.

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.

We make here a general presentation about how the formal verification of smart contracts works by explaining:

• How people secure their smart contracts without formal verification.
• How do formal tools typically work?
• How our solution coq-of-solidity works on a short example (an ERC-20 contract).
• Where LLMs could be the most useful, according to us, for formal verification work.

In this blog post, we continue our presentation about our formal verification tool for ◼️ Noir programs coq-of-noir. Noir is a Rust-like language to write programs designed to run efficiently in zero-knowledge environments. It has a growing popularity and a focus on providing optimized libraries for common needs, such as a base64 library using 🧠 field arithmetic that we use in this series of blog posts.

Here we present the details of our semantic rules to show that a Noir program has an expected behavior for any possible parameters. We focus, in particular, on our memory-handling approach and the definition of loops.