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.

In this blog post, we present what we do at Formal Land 🌲, what tools and services we are developing to provide more security for our customers 🦸. We believe that for critical applications such as blockchains (L1, L2, dApps) you should always use the most advanced technologies to find bugs, otherwise bad actors will do and overtake you in the never-ending race for security 🏎️.

Formal verification is one of the best techniques to ensure that your code is correct, as it checks every possible input ✨ of your program. For a long, formal verification was reserved for specific fields, such as the space industry 🧑‍🚀. We are making this technology accessible for the blockchain industry and general programming thanks to tools and services we develop, like coq-of-solidity and coq-of-rust.

In this blog post, we present our project to formally verify the implementation of the type checker for smart contracts of the 💧 Sui blockchain. The Sui blockchain uses the Move language to express smart contracts. This language is implemented in 🦀 Rust and compiles down to the Move bytecode that is loaded in memory when executing the smart contracts.

We will formally verify the part that checks that the bytecode is well-typed, so that when a smart contract is executed it cannot encounter critical errors. The type checker itself is also written in Rust, and we will verify it using the proof assistant Coq 🐓 and our tool coq-of-rust that translates Rust programs to Coq.

In this blog post we explain how we specify and formally verify a whole ERC-20 smart contract using our tool coq-of-solidity, which translates Solidity code to the proof assistant Coq 🐓.

The proofs are still tedious for now, as there are around 1,000 lines of proofs for 100 lines of Solidity. We plan to automate this work as much as possible in the subsequent iterations of the tool. One good thing about the interactive theorem prover Coq is that we know we can never be stuck, so we can always make progress in our proof techniques and verify complex properties even if it takes time ✨.

Formal verification with an interactive proof assistant is the strongest way to verify programs since:

• it covers all possible inputs and program states,
• it checks any kind of properties.

We continue to strengthen the security of smart contracts with our tool coq-of-solidity 🛠️. It checks for vulnerabilities or bugs in Solidity code. It uses formal verification with an interactive theorem prover (Coq 🐓) to make sure that we cover:

• all possible user inputs/storage states, even if there are infinite possibilities,
• for any security properties.

This is very important as a single bug can lead to the loss of millions of dollars in smart contracts, as we have regularly seen in the past, and we can never be sure that a human review of the code did not miss anything.

Our tool coq-of-solidity is one of the only tools using an interactive theorem prover for Solidity, together with Clear from Nethermind. This might be the most powerful approach to making code without bugs, as exemplified in this PLDI paper comparing the reliability of various C compilers. They found numerous bugs in each compiler except in the formally verified one!

In this blog post we show how we functionally specify and verify the _approve function of an ERC-20 smart contract. We will see how we prove that a refined version of the function is equivalent to the original one.

We continue to work on our open source formal verification tool for Solidity named coq-of-solidity 🛠️. Formal verification is the strongest form of code audits, as we verify that the code behaves correctly in all possible execution cases 🔍. We use the interactive theorem prover Coq to express and verify any kinds of properties.

We work by translating the Yul version of a smart contract to the formal language Coq 🐓, in which we then express the code specifications/security properties and formally verify them 🔄. The Yul language is an intermediate language used by the Solidity compiler and others to generate EVM bytecode. Yul is simpler than Solidity and at a higher level than the EVM bytecode, making it a good target for formal verification.

In this blog post we present the recent developments we made to simplify the reasoning 🧠 about Yul programs once translated in Coq.

Solidity is the most widely used smart contract language on the blockchain. As smart contracts are critical software handling a lot of money, there is a huge interest in finding all possible bugs before putting them into production.

Formal verification is a technique to test a program on all possible entries, even when there are infinitely many. This contrasts with the traditional test techniques, which can only execute a finite set of scenarios. As such, it appears to be an ideal way to bring more security to smart contract audits.

In this blog post, we present the formal verification tool coq-of-solidity that we are developing for Solidity. Its specificities are that:

1. It is open-source (GPL-3 for the translation, MIT for the proofs).
2. It uses an interactive theorem prover, the system Coq, to verify arbitrarily complex properties.

Here, we present how we translate Solidity code into Coq using the intermediate language Yul. We explain the semantics we use and what remains to be done.

The code is available in our fork of the Solidity compiler at github.com/formal-land/coq-of-solidity.

Formal verification is a technique to verify the absence of bugs in a program by reasoning from first principles. Instead of testing a program on examples, what covers a finite number of cases, formal verification checks all possible cases. It does so by going back to the definition of programming languages, showing why the whole code is correct given how each individual keyword behaves.

We will present this idea in detail and illustrate how it works for a very simple example.

In order to formally verify Python code in Coq our approach is the following:

1. Import Python code in Coq by running coq-of-python.
2. Write a purely functional simulation in Coq of the code.
3. Show that this simulation is equivalent to the translation.
4. Verify the simulation.

We will show in this article how we can merge the steps 2. and 3. to save time in the verification process. We do so by relying on the proof mode of Coq and unification.

Our mid-term goal is to formally specify the Ethereum Virtual Machine (EVM) and prove that this specification is correct according to reference implementation of the EVM in Python. This would ensure that it is always up-to-date and exhaustive. The code of this project is open-source and available on GitHub: formal-land/coq-of-python.

We are continuing to specify the Ethereum Virtual Machine (EVM) in the formal verification language Coq. We are working from the automatic translation in Coq of the reference implementation of the EVM, which is written in the language Python.

In this article, we will see how we specify the EVM in Coq by writing an interpreter that closely mimics the behavior of the Python code. We call that implementation a simulation as it aims to reproduce the behavior of the Python code, the reference.

In contrast to the automatic translation from Python, the simulation is a manual translation written in idiomatic Coq. We expect it to be ten times smaller in lines compared to the automatic translation, and of about the same size as the Python code. This is because the automatic translation needs to encode all the Python specific features in Coq, like variable mutations and the class system.

In the following article, we will show how we can prove that the simulation is correct, meaning that it behaves exactly as the automatic translation.

The code of this project is open-source and available on GitHub: formal-land/coq-of-python. This work follows a call from Vitalik Buterin for more formal verification of the Ethereum's code.