The formal specifications presented in this repository are written in eDSL, a domain-specific language for EVM specifications, which must be known in order to thoroughly understand the specifications. Refer to resources for background on our technology. Each of the specifications provides the eDSL specification template parameters. The full K reachability logic specifications are automatically derived by instantiating a specification template with these template parameters.
Run the following command in the root directory of this repository, and it will generate the full reachability logic specifications, under the directory specs, for the smart contract(s) in the <project> directory:
$ make -C <project> split-proof-tests
To prove that the specifications are satisfied by (the compiled EVM bytecode of) the target contracts, run the EVM verifier as follows:
$ make -C <project> test
The EVM verifier is part of the KEVM project. The following commands will successfully install it, provided that all of the dependencies are installed.
$ make -C <project> deps
For detailed instructions on installing and running the EVM verifier, see KEVM's Installing/Building and Example Usage pages.