Formalization of Ethereum Virtual Machine in Isabelle/HOL

This repository contains

• a Keccak-256 implementation in Isabelle/HOL KEC.thy
• a RLP implementation (in progress) RLP.thy
• an EVM implementation ContractSem.thy
• a relational semantics that captures the callee's nondeterministic behavior RelationalSem.thy
• some example verified contracts in example
• a parser that parses hex code and emits an Isabelle/HOL expression representing the program parser/hexparser.rb

When you see \<Rightarrow> in the source, try using the Isabelle2016 interface. There you see ⇒ instead.

Prerequisites

• Isabelle 2016
• lem
• OCaml 4.02.3
• opam 1.2.2
• yojson: use opam install yojson
• bignum: use opam install bignum
• easy-format: use opam install easy-format

Makefile goals

• make deed produces a verified PDF document for the Deed contract in output/document.pdf.
• make doc produces output/document.pdf as well as lem/*.pdf.
• make lem-thy compiles the Lem sources into Isabelle/HOL
• make lem-pdf compiles some of the Lem sources into PDF through LaTeX
• make all-isabelle checks all Isabelle/HOL sources (but not the ones compiled from Lem)
• make does everything above

Links

• For a bigger picture, see overview of Yoichi's formal verification efforts on smart contracts
• For updates, visit a gitter channel