Profile avatar
formalland.bsky.social
Formal verification for everyday-life applications We use math to ensure your code has no vulnerabilities For Rust, Solidity, zk circuits. We use Rocq. https://formal.land/
72 posts 38 followers 28 following
Regular Contributor
Active Commenter
Posts 23 Comments 27

🎊 Grant Announcement: Plonky3 in Rocq by Formal Land! Dive into how the team is establishing an extraction from Plonky3 to Rocq, and demonstrating its use by verifying relevant components of Plonky3-based zkVMs. x.com/FormalLand/s...

submitted 14 days ago • 1 comment

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

submitted 32 days ago • 1 comment

Our tool "coq-of-solidity" translates Solidity smart contracts to the formal language Rocq. What does it mean, and why is it important? 🧵

submitted 39 days ago • 1 comment

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

submitted 40 days ago • 0 comments

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.

submitted 41 days ago • 0 comments

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.

submitted 44 days ago • 0 comments

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.

submitted 45 days ago • 0 comments

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

submitted 48 days ago • 0 comments

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

submitted 50 days ago • 0 comments

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.

submitted 54 days ago • 1 comment

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

submitted 55 days ago • 1 comment

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

submitted 56 days ago • 1 comment

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

submitted 57 days ago • 1 comment

If you had some critical Rust code you wanted to formally verify, what would it be? Send it to us!

submitted 58 days ago • 0 comments

We are currently working on "coq-of-rust" to improve support for constant definitions by handling them as functions without parameters. This allows for handling special cases like constants in parametrized "impl" which were out of reach before.

submitted 58 days ago • 0 comments

submitted 59 days ago • 0 comments

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.

submitted 62 days ago • 1 comment

We wrote documentation about our coq-of-rust tool to formally verify 🦀 Rust programs, with an explanation of the "link" phase where we refine the translation to add types and name/trait resolution. This is here: formal.land/docs/tools/c...

submitted 70 days ago • 0 comments

We were happy to appear in Hacker News and Lobsters for coq-of-rust, our tool to formally verify Rust programs in Rocq! This is still in development, especially for the techniques to scale verification on large programs. Happy to talk if you have needs! The links: 👇

submitted 70 days ago • 1 comment

Continuing the development of `coq-of-rust` github.com/formal-land/... , to formally verify Rust programs, we also discover bugs in our tool. Let us dive into the technical details to give an example. Today, we found an incorrect handling of the trait implicit generics in their implementations. 👇

submitted 82 days ago • 1 comment

Our will with formal verification is to provide a complete solution for finding all vulnerabilities, before they become bug bounties or exploits. 💥

submitted 85 days ago • 0 comments

Slides about the work we are currently doing to improve our formal verification tool for Rust named "coq-of-rust": formal.land/slides/2025-... The goal is to make a full functional specification of Revm, the Rust implementation of the Ethereum's smart contract interpreter.

submitted 87 days ago • 0 comments

Here is a page showing the status of our project to formally specify Revm (Rest EVM) in Rocq using "coq-of'rust'. In short, we have the typing of the ADD instruction and its dependencies. Now, we need to handle the memory of the rest of the instructions! formal.land/docs/tools/c...

submitted 92 days ago • 0 comments