Ethereum Virtual Machine for interactive theorem provers (version 0.0.1)

I announce the version 0.0.1 of eth-isabelle project: a formalization of Ethereum Virtual Machine (EVM) for interactive theorem provers.

In this version,

• all EVM instructions are defined;
• the definitions pass 40,669 test cases from the standard VM tests (though I skipped 24 that run multiple contracts); and
• an interactive theorem prover Isabelle/HOL can use the definitions to prove safety properties of Ethereum smart contracts (in a plain brute-force, for now).

The definitions are in Lem so they should be portable to Coq and HOL4.

This release is a bare minimum intended as a basis for further development of various tools. From here on, a dozen different paths extend. So you are welcome if you are interested in building

• program logics for a stack machine with goto’s,
• verified static analyzers,
• verified optimizers,
• verified compilers, and of course,
• never broken Dapps.

I thank Sami Mäkelä for porting the definitions to Lem, and pointing out several mistakes.