Name		Name	Last commit message	Last commit date
Latest commit History 287 Commits
document		document
example		example
lem		lem
parser		parser
.gitignore		.gitignore
ContractEnv.thy		ContractEnv.thy
ContractSem.thy		ContractSem.thy
FeeSchedule.thy		FeeSchedule.thy
FunctionalCorrectness.thy		FunctionalCorrectness.thy
HP.thy		HP.thy
Instructions.thy		Instructions.thy
KEC.thy		KEC.thy
LICENSE		LICENSE
Makefile		Makefile
Memory.thy		Memory.thy
ModifiedPatricia.thy		ModifiedPatricia.thy
Parse.thy		Parse.thy
ProgramInAvl.thy		ProgramInAvl.thy
README.md		README.md
RLP.thy		RLP.thy
ROOT		ROOT
RelationalSem.thy		RelationalSem.thy
TODO		TODO
YellowPaper.thy		YellowPaper.thy
comment.sty		comment.sty
document_generation.sh		document_generation.sh
isabelle.sty		isabelle.sty
isabellesym.sty		isabellesym.sty
isabelletags.sty		isabelletags.sty
pdfsetup.sty		pdfsetup.sty
railsetup.sty		railsetup.sty

Repository files navigation

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

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

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 all-isabelle checks all Isabelle/HOL sources (but not the ones compiled from Lem)
make does everything above