The K-framework provides a reachability logic theorem prover that is parameterized by the langauge semantics. Instantiated with the KEVM, a complete formal semantics of the Ethereum Virtual Machine (EVM), the K prover yields a correct-by-construction deductive program verifer for the EVM. The EVM verifier takes an EVM bytecode and a specification as inputs, and automatically proves that the bytecode satisfies the specification, if it is the case. The EVM specification essentially specifies the pre- and post-conditions of the EVM bytecode in the form of reachability logic claims.
We present a domain-specific language (DSL) for the EVM specifications, called eDSL, to succintly specify the specifications. The eDSL consists of two parts: