Skip to main content

One post tagged with "simulation"

View All Tags

· 9 min read

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.