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

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.

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 👇

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

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

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

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

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

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!