🦄 Short introduction to Rocq | Formal Land
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.| formal.land
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.| Formal Land Blog
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.| Formal Land Blog
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.| formal.land
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.| Formal Land Blog
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.| Formal Land Blog
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.| formal.land
In this blog post, we present how we specify and verify the implementation of the ADD instruction of the EVM virtual machine in Rust.| formal.land
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.| formal.land
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.| Formal Land Blog
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.| Formal Land Blog
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.| Formal Land Blog
We make here a general presentation about how the formal verification of smart contracts works by explaining:| Formal Land Blog
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.| Formal Land Blog
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.| Formal Land Blog
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 o...| Formal Land Blog
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.| Formal Land Blog
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.| Formal Land Blog
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.| Formal Land Blog
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.| formal.land
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.| formal.land
We are starting to work on a new product, coq-of-python. The idea of this tool is, as you can guess, to translate Python code to the proof system Coq.| formal.land
At Formal Land our mission is to reduce the cost of finding bugs in software. We use formal verification, that is to say mathematical reasoning on code, to make sure we find more bugs than with testing. As part of this effort, we are working on a tool coq-of-rust to translate Rust code to Coq, a proof assistant, to analyze Rust programs. Here we present a technical improvement we made in this tool.| formal.land
