Guillaume Claret
@guillaume-claret.bsky.social
Founder/Security researcher at Formal Land
Formal verification in Rocq (PhD). Solitity/Rust/ZK
Discuss: https://calendly.com/guillaume-claret
Formal verification in Rocq (PhD). Solitity/Rust/ZK
Discuss: https://calendly.com/guillaume-claret
Reposted by Guillaume Claret
✨ 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...
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...
🥷 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...
formal.land
September 18, 2025 at 1:33 PM
✨ 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...
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...
Reposted by Guillaume Claret
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 a code extract in Rust:
August 8, 2025 at 3:17 PM
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 a code extract in Rust:
Reposted by Guillaume Claret
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 present the reasoning rules, as well as how to apply them to verify that an example has no under-constraints. ✅
The link 👇
July 31, 2025 at 1:49 PM
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 present the reasoning rules, as well as how to apply them to verify that an example has no under-constraints. ✅
The link 👇
Reposted by Guillaume Claret
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: 👇
LLZK is a zero-knowledge circuit language based on MLIR by Veridise. This work is funded by the Ethereum Foundation.
Link: 👇
July 30, 2025 at 3:23 PM
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: 👇
LLZK is a zero-knowledge circuit language based on MLIR by Veridise. This work is funded by the Ethereum Foundation.
Link: 👇
Reposted by Guillaume Claret
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: 👇
The main security property we are looking for is the absence of underconstraints. The link: 👇
July 30, 2025 at 9:15 AM
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: 👇
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.
Interactive provers are then the best to express ideas/build on top of a solid foundation. To handle the repetitive parts: LLMs + automation.
July 13, 2025 at 8:31 PM
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.
Interactive provers are then the best to express ideas/build on top of a solid foundation. To handle the repetitive parts: LLMs + automation.
Reposted by Guillaume Claret
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! 👇
This specification is in idiomatic Rocq but follows the structure of the Rust code. It includes the gas and versioning! 👇
July 13, 2025 at 8:24 PM
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! 👇
This specification is in idiomatic Rocq but follows the structure of the Rust code. It includes the gas and versioning! 👇
Reposted by Guillaume Claret
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: 👇
We finally achieved that for the ADD instruction! Here is what it looks like: 👇
July 3, 2025 at 2:28 PM
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: 👇
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 😂
I will go to NoirCon and ZK Hack. For now, at the WeWork to feel like home 😂
June 18, 2025 at 3:21 PM
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 😂
I will go to NoirCon and ZK Hack. For now, at the WeWork to feel like home 😂
Reposted by Guillaume Claret
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...
formal.land/blog/2025/06...
🦀 Beginning of translation of OpenVM to Rocq | Formal Land
Here, we present our beginning work of translating part of the OpenVM code to the proof assistant Rocq. The aim is to experiment around the formal verification of the zero-knowledge circuits of ...
formal.land
June 15, 2025 at 5:50 PM
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...
formal.land/blog/2025/06...
Reposted by Guillaume Claret
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 is what we are working on with Garden, our formal verification framework for circuits in Rocq.
The link: 👇
April 26, 2025 at 2:13 PM
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 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? 🧵
But first, how does the EVM work? 🧵
April 21, 2025 at 7:38 PM
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? 🧵
But first, how does the EVM work? 🧵
Reposted by Guillaume Claret
Our tool "coq-of-solidity" translates Solidity smart contracts to the formal language Rocq.
What does it mean, and why is it important? 🧵
What does it mean, and why is it important? 🧵
April 19, 2025 at 2:45 PM
Our tool "coq-of-solidity" translates Solidity smart contracts to the formal language Rocq.
What does it mean, and why is it important? 🧵
What does it mean, and why is it important? 🧵
Reposted by Guillaume Claret
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
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
April 18, 2025 at 12:32 PM
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
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
Reposted by Guillaume Claret
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.
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.
April 17, 2025 at 3:52 PM
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.
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.
Reposted by Guillaume Claret
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.
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.
🌱 Garden | Formal Land
Garden is a formal verification framework that helps you verify your zero-knowledge applications with ease.
formal.land
April 14, 2025 at 10:25 AM
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.
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.
Reposted by Guillaume Claret
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.
- A strong pressure to get things right,
- All the code is available as open-source,
- The market is rather open to new players.
April 13, 2025 at 12:07 PM
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.
- A strong pressure to get things right,
- All the code is available as open-source,
- The market is rather open to new players.
Reposted by Guillaume Claret
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! 👋
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! 👋
April 10, 2025 at 3:32 PM
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! 👋
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! 👋
Reposted by Guillaume Claret
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! 🥐
Hoping to see you at the Paris Blockchain Week event! 🥐
April 8, 2025 at 3:10 PM
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! 🥐
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.
The cost need to be competitive though compared to AWS.
April 4, 2025 at 11:42 AM
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.
The cost need to be competitive though compared to AWS.
Reposted by Guillaume Claret
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.
April 4, 2025 at 11:25 AM
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.
Reposted by Guillaume Claret
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/...
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
April 3, 2025 at 4:27 PM
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/...
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/...
Reposted by Guillaume Claret
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! 💪
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! 💪
April 2, 2025 at 9:41 AM
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! 💪
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! 💪
Reposted by Guillaume Claret
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: 👇
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: 👇
April 1, 2025 at 8:40 AM
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: 👇
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!
March 31, 2025 at 8:12 PM
We should make tutorials and documentations based on the new image generator!