✨ 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 will post more updates when the proof is complete! 🎄
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.
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).
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.
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/...
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
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.
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.
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.
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:
The blog post: formal.land/blog/2025/07...
Happy to discuss the proof strategy/choices of representation!
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: 👇
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.
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.
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:
Finally, we update the top of the stack with the result of "Impl_Uint.wrapping_add" applied to the two top elements!
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".
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.
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.
The functional specification (more verbose, partly because we unroll the macros):
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);
}
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: 👇
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.
