Skip to content

/ eth-acl2

An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.

Apache-2.0 License
2 stars 1 fork
Star
Watch
master
2 branches 0 tags
Go to file
Code
Clone

Use Git or checkout with SVN using the web URL.

Latest commit

@zchn
zchn Enable msize tests.
fec0f2f Jun 24, 2018
Enable msize tests.
fec0f2f

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
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.

About

An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.

Topics

ethereum verification formal-methods formalization proofs evm acl2

Resources

Readme

License

Apache-2.0 License

Releases

No releases published

Packages

No packages published

Contributors 2

  •  
  •  

Languages