Prove functional correctness of Ethereum smart contracts in higher-order logic.
When you clone this repository don't forget to git submodule update --init too.
Work in progress.
- The files in this repository are intended for use with the HOL theorem prover.
- An official executable specification of the Ethereum virtual machine can be found here.
- Another useful resources on the EVM is evm.codes.
- Define the machine
- Pass existing test suites
- Define a program logic (for use with decompilation into logic)
- Specify and verify some simple one-contract protocols (WETH, RocketSplit, etc.)
- ...