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:
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.
We are starting to work on a new product, coq-of-python. The idea of this tool is, as you can guess, to translate Python code to the proof system Coq.
We want to import specifications written in Python to a formal system like Coq. In particular, we are interested in the reference specification of Ethereum, which describes how EVM smart contracts run. Then, we will be able to use this specification to either formally verify the various implementations of the EVM or smart contracts.
All this effort follows a Tweet from Vitalik Buterin hoping for more formal verification of the Ethereum's code:
One application of AI that I am excited about is AI-assisted formal verification of code and bug finding.
Right now ethereum's biggest technical risk probably is bugs in code, and anything that could significantly change the game on that would be amazing.
— Vitalik Buterin
We will now describe the technical development of coq-of-python. For the curious, all the code is on GitHub: formal-land/coq-of-python.