iiinova — where your digital self keeps evolving

We will post more updates when the proof is complete! 🎄

000

To that end, we state that if the circuit runs until the end on a witness, then it must be the encoding with field elements of a Keccak computation. Frequent intermediate operations are showing that arrays hold boolean field elements, as well as manipulations of limbs of binary integers.

100

We verify these logical tricks by brute-forcing all the possible values for the booleans, as there are only up to five or six such booleans for each formula. The main property we show is that the circuit is deterministic (no under-constraints).

100

Then we write our proofs, trying to be careful to follow the organization of the original code, by verifying each loop independently and composing their behavior in a second step. A few logical tricks are used in the definition of Keccak to replace some XOR operations by equivalent additions.

100

We might choose to refine those choices later, once we better understand the bottlenecks in the proofs. Our base definitions are in github.com/formal-land/...

100

For now, we use rather simple data structures. For example, for field elements with use explicit Z elements with a modulo "p" operation, "p" being supposed as a prime number. For arrays, we use the total function of their indices, returning a default value when out of bounds

100

It is important to keep the original structure of the code, with explicit loops, in order to keep the number of equations small. It will be simpler to reason about loops rather than a larger number of equations. In addition, the loops are rather simple here in terms of invariants.

100

The Rust source code is available at github.com/Plonky3/Plon... For now, we translate it by hand to the corresponding constraints in Rocq in the Garden project github.com/formal-land/... We will ensure later with "coq-of-rust" that it corresponds to the original implementation.

100

The Keccak hash function, one of the most frequently used hash primitives in the Ethereum protocol, is implemented here efficiently using zero-knowledge constraints. This amounts to encoding boolean operations like XOR or shift using equations over polynomials of integers modulo a prime number.

100

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:

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 👇

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

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

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

It differs from what we were doing before, which was generating a typed and executable Rocq version, but without making explicit the non-aliasing and with a quite verbose version, making it difficult to use for the proofs.

000

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

1. Continue to verify a functional definition for the rest if the EVM instructions. 2. Show that this functional definition is equivalent to a semantics for the EVM in Rocq. There is at least one such project that we could show as equivalent to a reference implementation.

000

For the rest of the instructions, we have a typed representation in Rocq generated with the help of "coq-of-rust". However, we do not have a clear idiomatic and functional definition like for the instruction ADD. From there, we can go in two directions:

110

Finally, we update the top of the stack with the result of "Impl_Uint.wrapping_add" applied to the two top elements!

100

We first try to consume a "VERYLOW" amount of gas. If it fails, we return the "OutOfGas" error message. Otherwise, we pop one element from the stack and ask for a reference to the next one. If there are not enough elements, we return "StackUnderflow".

100

In our functional specification, the first line: Output.Success tt says that there can be no runtime failures (no panics!), assuming none of the provided methods panic. This is an important safety property. The rest describes how the ADD instruction behaves.

100

One of the difficulties here is that the code is very abstract. The types of the stack or gas field are not defined, nor are the functions to manipulate them. Instead, they are provided as trait implementations. We need to specify them somehow to say they admit a functional specification.

100

The functional specification (more verbose, partly because we unroll the macros):

100

The ADD instruction as implemented in Rust: pub fn add<WIRE: InterpreterTypes, H: Host + ?Sized>( interpreter: &mut Interpreter<WIRE>, _host: &mut H, ) { gas!(interpreter, gas::VERYLOW); popn_top!([op1], op2, interpreter); *op2 = op1.wrapping_add(*op2); }

100

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

It is a bit unusual when writing functional code, as it optionally returns a reference to be used later to mutate some state (the top element of the stack). We obtained a proof-of-concept specification for this kind of code and are iterating on it to handle the ADD example cleanly.

100

This code is quite complex because: - There are macros "!". But these can be quickly unfolded. - It depends on traits, which are abstract. The type of the pop function used internally: fn popn_top<const POPN: usize>(&mut self) -> Option<([U256; POPN], &mut U256)>;

100

We take the real-world example of the code of the ADD instruction in Revm: pub fn add<WIRE: InterpreterTypes, H: Host + ?Sized>( interpreter: &mut Interpreter<WIRE>, _host: &mut H, ) { gas!(interpreter, gas::VERYLOW); popn_top!([op1], op2, interpreter); *op2 = op1.wrapping_add( *op2); }

100

Guillaume Claret @guillaume-claret.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

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 😂

Formal Land @formalland.bsky.social · 15/05/2025

Thanks for the notice! Happy to contribute to making zero-knowledge really safe, and happy to discuss if you have questions!

010

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

github.com/formal-land/... Our first target is Plonky3-like circuits, with the verification of the Blake3 AIR primitive. 🔍 Feel free to chat with us if you have needs! 📢

github.com

GitHub - formal-land/garden: Make your zero-knowledge applications safe with formal verification! 🍀

Make your zero-knowledge applications safe with formal verification! 🍀 - formal-land/garden

010

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

This truly means the ability to write software without bugs! 🎉🎉🎉 To make the bridge between programming languages like Solidity and formal languages like Rocq we need a translator (or compiler) to translate Solidity to the Rocq format.

110

On the other side, formal languages like Rocq are designed to express software specifications, like "the smart contract can never end up in a situation where the funds are blocked", and verify them on *all* possible inputs. This process is called formal verification. ✅

100

Solidity is the language used to write smart contracts on Ethereum and compatible blockchains. These are rather short programs (< 5,000 lines) with high security risks. 🥷 Smart contracts handle real money, and a single bug often means the loss of millions of dollars! 💸

100

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 @atlascomputing.bsky.social · 18/04/2025

Reposted by Formal Land

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.

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.

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.

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