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
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 😂
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? 🧵
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!
Our working space with the anime painting mode in Paris :)
March 31, 2025 at 5:20 PM
Our working space with the anime painting mode in Paris :)
There are so many features in the Rust language! Today we add support for casts from enums to integers in coq-of-rust.
It is possible to define an explicit value for some of the fields. The other ones are implicitly incremented by one following the ordering.
It is possible to define an explicit value for some of the fields. The other ones are implicitly incremented by one following the ordering.
February 17, 2025 at 10:27 AM
There are so many features in the Rust language! Today we add support for casts from enums to integers in coq-of-rust.
It is possible to define an explicit value for some of the fields. The other ones are implicitly incremented by one following the ordering.
It is possible to define an explicit value for some of the fields. The other ones are implicitly incremented by one following the ordering.
Exciting progress on the formal specification of Revm, the Rust implementation of the EVM for Ethereum! 🚀
Yesterday, we completed adding type information to our Rocq/Coq translation of the gas file. This milestone means our process is now functional with real examples. Check out the details below:
Yesterday, we completed adding type information to our Rocq/Coq translation of the gas file. This milestone means our process is now functional with real examples. Check out the details below:
February 11, 2025 at 10:06 AM
Exciting progress on the formal specification of Revm, the Rust implementation of the EVM for Ethereum! 🚀
Yesterday, we completed adding type information to our Rocq/Coq translation of the gas file. This milestone means our process is now functional with real examples. Check out the details below:
Yesterday, we completed adding type information to our Rocq/Coq translation of the gas file. This milestone means our process is now functional with real examples. Check out the details below: