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.

We are continuing our formal verification work for the implementation of the type-checker of the Move language in the 💧 Sui blockchain. We verify a manual translation in the proof system 🐓 Coq of the 🦀 Rust code of the Move checker as available on GitHub.

In this blog post, we present in detail the verification of a particular function AbstractStack::pop_eq_n that manipulates 📚 stacks of types to show that it is equivalent to its naive implementation.

All the code presented here is on our GitHub at github.com/formal-land/coq-of-rust 🧑‍🏫.

In this series of blog posts, we present our development of a formal verification tool for the ◼️ Noir smart contract language. It is particularly suited to writing zero-knowledge applications, providing primitive constructs such as a Field type to write programs that run efficiently as circuits. Having a formal verification for Noir enables the development of applications holding a large amount of money in this language, as it ensures that the code is correct with a mathematical level of certainty.

In this first post, we present how we translate Noir code to the 🐓 Coq proof system. We explore a translation after monomorphization and then at the HIR level. Note that we are interested in verifying programs written in Noir. The verification of the Noir compiler itself is a separated topic.

All our code is available as open-source on github.com/formal-land/coq-of-noir, and you are welcome to use it. We also provide all-included audit services to formally verify your smart contracts using coq-of-noir.

In this blog post, we detail the continuation of our work to formally verify the ⚈ Smoo.th library, which is an optimized implementation of elliptic curve operations in Solidity. We use our tool coq-of-solidity, representing any Solidity code in the generic proof assistant 🐓 Coq, to verify the code for any execution path.

In particular, we cover the changes we made to use unoptimized Yul code and how we made a functional representation of the loop to compute the most significant bit of the scalars.

We bring you the highest possible level of security 🦸 for your blockchain applications by using formal verification ✨ optimized by AI solutions to keep the cost down. We believe that for systems holding a lot of value 💰, it is necessary to use the most advanced techniques ⚛️ to ensure their security; otherwise attackers with large means (like North Korea 🇰🇵, but not only) will be able to steal or damage the system by using these techniques themselves.

In this blog post we present how we work with customers to integrate full formal verification in their workflow and ensure that their code is secure in the best possible way.