A tool to verify solidity contracts via translation to F*.
There are two tools in this distribution:
evmstar is a tool that reads in an EVM program and translates it
to F*. The source for this tool is in
the src/evmstar directory. To build it, install batteries via opam, and
then run make in that directory. To run it, type
./EvmStar.exe -i path/to/pgm.evm Type EvmStar.exe -h for the tool's annotation functionality.
solidstar is a tool that translates Solidity contracts to F*.
The source for this tool is in the src/solidstar directory. To
build it, install menhir, PCRE and ulex via opam, and then
run make in that directory. To run it, type
./soliditystar.native x.solSome small examples are given in the /examples directory.
Larger examples of bytecodes and contracts can be downloaded using the scripts in data/scripts. You need mkdir data/bytecode and data/contracts the directories already.
For some context, see:
Other links to attacks:
EVM tutorial:
Reference:
Resources: