Ethereum Virtual Machine for Coq (v0.0.2)

Yoichi Hirai
Mar 5, 2017 · 2 min read

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.

Image for post
Image for post
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

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.

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch

Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore

Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store