✨ New work from our grantee @formalland.bsky.social, formally verifying ZK circuits for zkVMs! Their new blog post presents how to pretty-print the constraints from a Plonky3 circuit, ensuring their modeling is correct. formal.land/blog/2025/08...

We are currently formally verifying, in Rocq, the implementation of the Keccak hash function from Plonky3 in AIR. Here is a code extract in Rust:

Here is our last blog post about the formal verification of LLZK circuits in Rocq. We present the reasoning rules, as well as how to apply them to verify that an example has no under-constraints. ✅ The link 👇

Here is a new blog post on how we define the LLZK operator in the formal verification language Rocq, to assert that there are no under-constraints. LLZK is a zero-knowledge circuit language based on MLIR by Veridise. This work is funded by the Ethereum Foundation. Link: 👇

Here is a blog post where we explain how we translate the LLZK zero-knowledge circuit language to the proof system Rocq, in order to formally verify such circuits. The main security property we are looking for is the absence of underconstraints. The link: 👇

What I believe is the best way to make formal verification tools that scales is to first capture the intents of the programmers, but in a 💯 rational way. Interactive provers are then the best to express ideas/build on top of a solid foundation. To handle the repetitive parts: LLMs + automation.

We are currently writing a whole EVM specification in the Rocq language that we prove equivalent to the original implementation in Revm. This specification is in idiomatic Rocq but follows the structure of the Rust code. It includes the gas and versioning! 👇

One of our primary targets these days (months) is to make a functional specification for the Rust implementation of the EVM (Ethereum Virtual Machine) named Revm. We finally achieved that for the ADD instruction! Here is what it looks like: 👇

I am happy to have safely arrived in Berlin for all the side events of the Blockchain Week and to discuss formal verification and ZK! I will go to NoirCon and ZK Hack. For now, at the WeWork to feel like home 😂

A new blog post about our work to translate the Rust code of OpenVM to Rocq, with the aim of formally verifying that the circuits have no under-constraints: formal.land/blog/2025/06...

You want to formally verify your ZK circuits in a scalable way? This is what we are working on with Garden, our formal verification framework for circuits in Rocq. The link: 👇

Vitalik, the founder of Ethereum, proposed the idea of migrating smart contracts from EVM to RISC-V, for performance reasons when going to ZK execution layers. But first, how does the EVM work? 🧵

Our tool "coq-of-solidity" translates Solidity smart contracts to the formal language Rocq. What does it mean, and why is it important? 🧵

Atlas Computing Symposium : Rust (Friday, May 2, 2025 - Ottawa, Canada) lu.ma/umi3g2wc Speaker highlight: Guillaume Claret is a security researcher and the founder of @formalland.bsky.social, a company specializing in the application of formal methods to critical code. #rustlang

The reason we develop formal verification tools is to provide the best value for code audits. With our "coq-of-solidity" and "coq-of-rust" projects, it is possible to verify Solidity and Rust projects in an integrated manner in Rocq to prevent most vulnerabilities.

Garden is our project to formally verify zero-knowledge circuits: formal.land/docs/tools/g... Reach out to us if you are interested in auditing your circuits! We are happy to contribute to the security of the advanced operations written in zero-knowledge technology.

We believe Web3 is the best space for the development of new auditing tools, as there is a unique combination of: - A strong pressure to get things right, - All the code is available as open-source, - The market is rather open to new players.

Paris Blockchain Week 2025 is coming to an end. This was a great conference with many interesting side-events located along the river or the Louvres in Paris, for the best view. See you next year! 👋

At Formal Land, we focus on providing the best level of security by developing advanced auditing solutions with formal verification. 🛡️ Hoping to see you at the Paris Blockchain Week event! 🥐

A random idea to make a blockchain with "Proof of Useful Work": using ZK to verify some computations that are distributed to the network, acting as a cloud provider. The cost need to be competitive though compared to AWS.

We are happy to attend the "AI and Math" day in Paris with a lot of presentations about the application of LLMs to formal proofs in Rocq or Lean, from experts in the field.

We like to have numbers to measure our progress while coding. Here is the list of EVM instructions from the Rust Revm implementation that we have successfully translated to a typed version in Rocq: github.com/formal-land/...

Having better support for constants in "coq-of-rust" is now done! ✌️ Another improvement: handling the native binary operators as normal functions to uniformize a lot of code on the proving side. Now, we reach a new difficulty: handling implicit coercions from &[T; N] to &[T] 🤔 A new task to do! 💪

Rocq has this rarely known feature, and mathematicians hate it for that. (This is not clickbait 😆) Impredicative Set allows to quantify over types of values while still being at the same level. This leads to paradox for most mathematicians but not in Rocq! Here is what follows: 👇

We should make tutorials and documentations based on the new image generator!

Our working space with the anime painting mode in Paris :)

Video of the Isar Aerospace "Full Spectrum" Launch at Andøya. 📸 video: @isaraerospace / @AndoyaSpace

We continue working on our coq-of-rust project to formally verify any Rust programs with the Rocq theorem prover. For critical applications, this enables making sure the code is free of vulnerabilities, given the right specification.

I was happy to attend the ZKProof conference @zkproof.org , with many discussions with the zero-knowledge cryptographers and formal verification people! Interested to follow what happens with the verified verifier project!

On this YouTube channel there are the videos of the discussions about formal verification for zero-knowledge by the Ethereum Foundation: youtube.com/@verifiedzkevm Today there were interesting presentations about verification for cryptographic primitives that should be online soon.

We have to be honest and say when things are working well. Congrats to SpaceX and the US for the last landing of astronauts! www.spacex.com/launches/mis...

An "awsome list" of blockchain projects built in Rust: github.com/rust-in-bloc... 🔍

Live in four hours, the intro lesson of Thierry Coquand, creator of Coq/Rocq, in Colège de France in Paris: www.college-de-france.fr/fr/agenda/le... (in French, hopefully with subtitles; the buffet should be good also! 🙂)

Here are two areas where we think innovation in formal methods can have more space to grow: - Building methodologies that use AI, which is good at generating simple and boring code with 95% correctness. - Leveraging the dependent types/unification engine of advanced provers like Rocq/Lean.

Continuing the development of `coq-of-rust` github.com/formal-land/... , to formally verify Rust programs, we also discover bugs in our tool. Let us dive into the technical details to give an example. Today, we found an incorrect handling of the trait implicit generics in their implementations. 👇

Our will with formal verification is to provide a complete solution for finding all vulnerabilities, before they become bug bounties or exploits. 💥

In Rocq, there are three kinds of visibility for definitions: local, export, and global. Local definitions are specific to the current file; exports are explicitly activated with an "Import," and globals are transitively added following the dependencies. When does it matter? 👇

Slides about the work we are currently doing to improve our formal verification tool for Rust named "coq-of-rust": formal.land/slides/2025-... The goal is to make a full functional specification of Revm, the Rust implementation of the Ethereum's smart contract interpreter.

Interesting to see that 3FS, the newly released file system by DeepSeek, got designed with the help of formal methods using the P system: github.com/deepseek-ai/... They seem to really use all the possible levers to get an AI better than the competition!!

Meetup intéressant à Paris pour apprendre à écrire ses premiets smart contracts Ethereum le 10 Mars 2025 : www.meetup.com/ethereum-fra...

Here is a page showing the status of our project to formally specify Revm (Rest EVM) in Rocq using "coq-of'rust'. In short, we have the typing of the ADD instruction and its dependencies. Now, we need to handle the memory of the rest of the instructions! formal.land/docs/tools/c...

Il y aura des cours de Thierry Coquand (créateur de Coq/Rocq) cette année au Collège de France ! Début le 13 Mars et libre d'accès sur place (Paris) ou en ligne. En Français uniquement ! www.college-de-france.fr/fr/chaire/th...

Zero-knowledge circuits are very hard to get right without formal verification. That is why we have focused a lot on this area lately, building technologies to verify Circom circuits and the like.

We believe that the formal specification of smart contracts, that is a requirement for good formal verification and audits, is still not fully developed and are going to push in this direction! The first target: defining "stealing" 🦹‍♂️

There are so many features in the Rust language! Today we add support for casts from enums to integers in coq-of-rust. It is possible to define an explicit value for some of the fields. The other ones are implicitly incremented by one following the ordering.

We are happy we will be presenting our work on the formal verification of Rust programs with coq-of-rust at Ottawa in May, together with most of the other FV tools for Rust. This event comes with a push from DARPA for more Rust and formal methods in critical code. The link: lu.ma/umi3g2wc?tk=...

Today's work: defining in Rocq enough semantics for memory allocation on stack so that we can prove this Rust file github.com/bluealloy/re... to be equivalent to a purely functional version in Rocq.

Exciting progress on the formal specification of Revm, the Rust implementation of the EVM for Ethereum! 🚀 Yesterday, we completed adding type information to our Rocq/Coq translation of the gas file. This milestone means our process is now functional with real examples. Check out the details below:

Today's work: adding more automation to coq-of-rust so that we can build a typed representation of github.com/bluealloy/re... in a very fluid manner. The end goal: having a framework to formally verify Rust code both at scale and for arbitrary code.