iiinova — where your digital self keeps evolving

Reposted by Formal Land

EF Ecosystem Support Program @ef-esp.bsky.social · 18/09/2025

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

formal.land

🥷 Pretty-printing of Rust ZK constraints | Formal Land

Many zkVMs are implemented in Rust, using the Plonky3 library to describe their circuits. While Rust is efficient and expressive for describing complex circuits, it is a complex language when it comes...

043

Formal Land @formalland.bsky.social · 08/08/2025

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:

111

Formal Land @formalland.bsky.social · 31/07/2025

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 👇

111

Formal Land @formalland.bsky.social · 30/07/2025

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: 👇

111

Formal Land @formalland.bsky.social · 30/07/2025

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: 👇

111

Formal Land @formalland.bsky.social · 13/07/2025

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! 👇

111

Formal Land @formalland.bsky.social · 03/07/2025

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: 👇

121

Formal Land @formalland.bsky.social · 18/06/2025

Until now, with "coq-of-rust", our translation tool from Rust to the formal system Rocq, we have mostly focusing on the first phase of the translation: handling the names, the types, and the traits. We are now starting to work on the second phase, to handle the memory aliases. 👇

110

Reposted by Formal Land

Guillaume Claret @guillaume-claret.bsky.social · 18/06/2025

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 😂

011

Formal Land @formalland.bsky.social · 26/04/2025

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: 👇

111

Formal Land @formalland.bsky.social · 19/04/2025

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

111

Reposted by Formal Land

Atlas Computing @atlascomputing.bsky.social · 18/04/2025

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

033

Formal Land @formalland.bsky.social · 17/04/2025

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.

011

Formal Land @formalland.bsky.social · 14/04/2025

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.

formal.land

🌱 Garden | Formal Land

Garden is a formal verification framework that helps you verify your zero-knowledge applications with ease.

011

Formal Land @formalland.bsky.social · 13/04/2025

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.

011

Formal Land @formalland.bsky.social · 10/04/2025

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! 👋

011

Formal Land @formalland.bsky.social · 08/04/2025

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! 🥐

031

Formal Land @formalland.bsky.social · 04/04/2025

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.

111

Formal Land @formalland.bsky.social · 03/04/2025

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

github.com

121

Formal Land @formalland.bsky.social · 02/04/2025

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! 💪

131

Formal Land @formalland.bsky.social · 01/04/2025

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: 👇

123

Formal Land @formalland.bsky.social · 31/03/2025

If you had some critical Rust code you wanted to formally verify, what would it be? Send it to us!

000

Formal Land @formalland.bsky.social · 31/03/2025

We are currently working on "coq-of-rust" to improve support for constant definitions by handling them as functions without parameters. This allows for handling special cases like constants in parametrized "impl" which were out of reach before.

010

Formal Land @formalland.bsky.social · 27/03/2025

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.

151

Formal Land @formalland.bsky.social · 19/03/2025

We wrote documentation about our coq-of-rust tool to formally verify 🦀 Rust programs, with an explanation of the "link" phase where we refine the translation to add types and name/trait resolution. This is here: formal.land/docs/tools/c...

formal.land

Links | Formal Land

The "links" phase is the first refinement step we do in order to simplify the code generated by coq-of-rust and to give it a semantics.

040

Formal Land @formalland.bsky.social · 19/03/2025

We were happy to appear in Hacker News and Lobsters for coq-of-rust, our tool to formally verify Rust programs in Rocq! This is still in development, especially for the techniques to scale verification on large programs. Happy to talk if you have needs! The links: 👇

120

Formal Land @formalland.bsky.social · 07/03/2025

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

github.com

GitHub - formal-land/coq-of-rust: Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦 - formal-land/coq-of-rust

131

Formal Land @formalland.bsky.social · 04/03/2025

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

011

Formal Land @formalland.bsky.social · 02/03/2025

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.

formal.land

021

Formal Land @formalland.bsky.social · 25/02/2025

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

formal.land

Revm Project | Formal Land

All the code of this project is available on github.com/formal-land/coq-of-rust/tree/main/CoqOfRust/revm

011

Formal Land @formalland.bsky.social · 20/02/2025

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.

121

Formal Land @formalland.bsky.social · 14/02/2025

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

lu.ma

Symposium on Formal Methods for RUST at ICSE 2025 · Luma

The event Today, critical infrastructure is vulnerable to both malicious attacks and unintended failures, and these risks are expected to grow in the…

021

Formal Land @formalland.bsky.social · 12/02/2025

The interest is growing in the use of AI to help formally verify code. There are still a lot of unknowns and possibilities, especially if we consider what would be possible with efforts as large as for Cursor/Copilot ✨. It might open the door for affordable formal verification! 🚀

010

Formal Land @formalland.bsky.social · 28/01/2025

We continue improving our formal verification tool coq-of-rust for Rust, working on better support for references. If you have critical Rust code that you want to definitely check for vulnerabilities, please contact us!

021

Reposted by Formal Land

Cryptography.academy @cryptoacademy42.bsky.social · 26/01/2025

We educate people about cryptography, and apply techniques like formal verification to build verified primitives.

021

Formal Land @formalland.bsky.social · 17/01/2025

Why is formal verification important for ZK circuits? One of the main security properties is not to be under-constrained. Otherwise, someone can come up with a proof of execution that does not do what is expected (like transferring all the money to itself), and your verifier will accept it!

100

Formal Land @formalland.bsky.social · 08/01/2025

Here is a blog post about an experiment we are doing with LLMs: writing down how we think when writing a Rocq proof, with the aim of getting a VSCode extension that can use these intuitions. formal.land/blog/2025/01...

formal.land

🤖 Annotating what we are doing for an LLM to pick up | 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 th...

011

Formal Land @formalland.bsky.social · 25/12/2024

A new blog post about our formal verification project for the 👻Circom zero-knowledge language: formal.land/blog/2024/12... How strategy: using the interactive proof system 🐓 Coq to be able to formally verify any kind of circuits!

formal.land

👻 Translation of Circom to Coq | Formal Land

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

110

Formal Land @formalland.bsky.social · 20/12/2024

A new blog post presenting smart contract security and formal verification in general, as well as possible future improvements in current tools: formal.land/blog/2024/12...

formal.land

🦄 How does formal verification of smart contracts work? | Formal Land

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

010

Formal Land @formalland.bsky.social · 18/12/2024

Here we published the list of auditing reports we made: formal.land/docs/audit We only do formal verification audits to be focused. Hoping for more Rust/Solidity audits next year!

formal.land

🛡️ Audit Reports | Formal Land

Reports

010

Formal Land @formalland.bsky.social · 13/12/2024

Here is a presentation video for our `coq-of-solidity` tool to formally verify smart contracts: www.canva.com/design/DAGZL... 📽️ The tool (open-source): github.com/formal-land/... Contact us for any questions!

020

Formal Land @formalland.bsky.social · 12/12/2024

At Formal Land, we help you make certain that your Web3 projects are safe. To that end, we use formal verification, which is the only way to verify code for 100% of execution cases. A project we are verifying these days is the Sui @suinetwork.bsky.social type-checker for the Move language. 👇

100