pirapira / eth-isabelle Public

Notifications You must be signed in to change notification settings
Fork 42
Star 239

A Lem formalization of EVM and some Isabelle/HOL proofs

239 stars 42 forks Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 125 Commits
example		example
ContractEnv.thy		ContractEnv.thy
ContractSem.thy		ContractSem.thy
EVM.thy		EVM.thy
FeeSchedule.thy		FeeSchedule.thy
HP.thy		HP.thy
Instructions.thy		Instructions.thy
KEC.thy		KEC.thy
LICENSE		LICENSE
Memory.thy		Memory.thy
ModifiedPatricia.thy		ModifiedPatricia.thy
Parse.thy		Parse.thy
README.md		README.md
RLP.thy		RLP.thy
RelationalSem.thy		RelationalSem.thy
TODO		TODO
YellowPaper.thy		YellowPaper.thy

Repository files navigation

Formalization of Ethereum Virtual Machine in Isabelle/HOL

The status is very immature. Currently a Coq project about EVM bytecode verification is being ported here. The directory also contains

a Keccak-256 implementation in Isabelle/HOL KEC.thy
a RLP implementation (in progress) RLP.thy

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

About

A Lem formalization of EVM and some Isabelle/HOL proofs

Report repository

Releases

Packages

No packages published

Contributors 4

Languages