We make here a general presentation about how the formal verification of smart contracts works by explaining:

• How people secure their smart contracts without formal verification.
• How do formal tools typically work?
• How our solution coq-of-solidity works on a short example (an ERC-20 contract).
• Where LLMs could be the most useful, according to us, for formal verification work.

In this blog post, we continue our presentation about our formal verification tool for ◼️ Noir programs coq-of-noir. Noir is a Rust-like language to write programs designed to run efficiently in zero-knowledge environments. It has a growing popularity and a focus on providing optimized libraries for common needs, such as a base64 library using 🧠 field arithmetic that we use in this series of blog posts.

Here we present the details of our semantic rules to show that a Noir program has an expected behavior for any possible parameters. We focus, in particular, on our memory-handling approach and the definition of loops.

We are continuing our formal verification work for the implementation of the type-checker of the Move language in the 💧 Sui blockchain. We verify a manual translation in the proof system 🐓 Coq of the 🦀 Rust code of the Move checker as available on GitHub.

In this blog post, we present in detail the verification of a particular function AbstractStack::pop_eq_n that manipulates 📚 stacks of types to show that it is equivalent to its naive implementation.

All the code presented here is on our GitHub at github.com/formal-land/coq-of-rust 🧑‍🏫.

In this series of blog posts, we present our development of a formal verification tool for the ◼️ Noir smart contract language. It is particularly suited to writing zero-knowledge applications, providing primitive constructs such as a Field type to write programs that run efficiently as circuits. Having a formal verification for Noir enables the development of applications holding a large amount of money in this language, as it ensures that the code is correct with a mathematical level of certainty.

In this first post, we present how we translate Noir code to the 🐓 Coq proof system. We explore a translation after monomorphization and then at the HIR level. Note that we are interested in verifying programs written in Noir. The verification of the Noir compiler itself is a separated topic.

All our code is available as open-source on github.com/formal-land/coq-of-noir, and you are welcome to use it. We also provide all-included audit services to formally verify your smart contracts using coq-of-noir.

In this blog post, we detail the continuation of our work to formally verify the ⚈ Smoo.th library, which is an optimized implementation of elliptic curve operations in Solidity. We use our tool coq-of-solidity, representing any Solidity code in the generic proof assistant 🐓 Coq, to verify the code for any execution path.

In particular, we cover the changes we made to use unoptimized Yul code and how we made a functional representation of the loop to compute the most significant bit of the scalars.

We bring you the highest possible level of security 🦸 for your blockchain applications by using formal verification ✨ optimized by AI solutions to keep the cost down. We believe that for systems holding a lot of value 💰, it is necessary to use the most advanced techniques ⚛️ to ensure their security; otherwise attackers with large means (like North Korea 🇰🇵, but not only) will be able to steal or damage the system by using these techniques themselves.

In this blog post we present how we work with customers to integrate full formal verification in their workflow and ensure that their code is secure in the best possible way.

In this blog post, we present the formal verification effort we started to show the absence of bugs in the ⚈ Smoo.th library, a library for optimized 〰️ elliptic curve operations in Solidity. We are using our tool coq-of-solidity to make this non-trivial verification using the generic proof assistant 🐓 Coq.

The Smoo.th library is interesting as elliptic curves are at the core of many cryptographic protocols, including authentication protocols, and having a generic and fast implementation simplifies the development of dApps in environments with missing pre-compiled (like L1s) or missing circuits (like zero-knowledge layers).

From a verification point of view, it is very challenging as it combines low-level operations (hand-optimized Yul code with bit shifts, inlined functions, ...) with higher-level reasoning on elliptic curves and arithmetic 💪.

We present improvements we made to our tool coq-of-solidity to formally verify Solidity smart contracts for any advanced properties, relying on the proof assistant 🐓 Coq. The idea is to be able to prove the full absence of bugs ✨ in very complex contracts, like L1 verifiers for zero-knowledge L2s 🕵️, or contracts with very large amounts of money 💰 (in the billions).

In this blog post, we present how we developed an effect inference mechanism to translate optimized Yul code combining variable mutations and control flow with loops and nested premature returns (break, continue, and leave) to a clean 🧼 purely functional representation in the proof system Coq.

In the previous blog post, we have seen how we represent side-effects from the Rust code of the Sui's Move type-checker of bytecode in Coq. This translation represents about 3,200 lines of Coq code excluding comments. We need to trust that this translation is faithful to the original Rust code, as we generate it by hand or with GitHub Copilot.

In this blog post, we present how we test this translation to ensure it is correct by running the type-checker on each opcode of the Move bytecode and comparing the results with the Rust code, testing the success and error cases.

We are working on formally verifying the 🦀 Rust implementation of the Move type-checker for bytecode in the proof system 🐓 Coq. You can find the code of this type-checker in the crate move-bytecode-verifier.

This requires translating all the Rust code in idiomatic Coq on which we will write our specifications and proofs. We write this translation by hand relying as much as possible on generative AI tools such as GitHub Copilot, as there are many particular cases. We plan, eventually, to prove it equivalent to the translation automatically generated by coq-of-rust.

In this blog post we present how we organize our 🔮 monad to represent the side-effects used in this Rust code. We believe this organization should work for other Rust projects as well.