Ethereum Virtual Machine for Coq (v0.0.2)

Here is the version 0.0.2 of eth-isabelle project. Now it can produce a Coq definition of the Ethereum Virtual Machine. The project provides a formal definition of the Ethereum Virtual Machine for interactive theorem provers. So far, the project provided the definition for Isabelle/HOL and HOL4. From version 0.0.2, the Coq version is available. Now it should be possible in Coq to prove Ethereum smart contracts correct.

The logo of Coq (distributed under LGPL).

The Coq version of the EVM definition is highly experimental because of the way it is generated. The original definition is written in a language called Lem, and the original is translated into different interactive theorem provers. I hear that Lem works well with HOL4 and Isabelle/HOL but that Coq extraction is harder to control. Sami Mäkelä spent a lot of time adjusting the Lem definitions so that the Coq extraction passes syntax & type-checking. The HOL extraction is in a similar state.

The development is in an early stage, so any suggestion is welcome. The definition should be able to run a program on EVM until it returns, fails or calls something.

After cloning the project and putting the Lem executable (lem) in the PATH,

make lem-coq

should generate the Coq version. With /usr/local/share/lem/coq-lib compiled,

cd lem
make

should compile the Coq EVM definition.

Currently, the Coq version has no theorems built on top. Some Isabelle proofs are in example directory using the Isabelle version.