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:
- It is open-source (GPL-3 for the translation, MIT for the proofs).
- 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/solidity.