An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
books
repos
scripts
.gitignore
.travis.yml
LICENSE
README.md

README.md

eth-acl2 Build Status

This is still a prototype, see issue #1, issue #2 and issue #3 for things to do to make it complete.

In addition to that, Kevin is primarily focusing on #4 and #5.

Long term, #6 is also desirable.