Virtual Machines

KEVM rationale

The KEVM devnet is based on the K framework, a system for specifying languages and virtual machines and then deriving tools for these languages such as interpreters, type checkers, equivalence checkers, and debuggers. It can be used to create both static and dynamic analysis tools.

KEVM is a specification of the EVM (Ethereum Virtual Machine) in K.

KEVM is also an interpreter for EVM, automatically derived from the KEVM specification. You could say that the K specification of EVM is the “source code” for the interpreter. But it is much more than that. KEVM can be used to prove that smart contracts are correct. This is done by specifying a contract’s desired properties in K, combining the contract with the KEVM specification, and then using the K framework to verify those properties. KEVM can be used to check for errors such as integer over and under flows, stack over and under flows, out-of-gas, and other contract generic properties. You can also verify more targeted properties for specific contracts.

When you run a smart contract on the devnet using the devnet wallet, the devnet will send the contract to the KEVM interpreter to be executed. This interpreter is the only part of the devnet that is based on the K framework. But because the interpreter is generated from the K specification, you can use K (and KEVM) to verify your smart contracts before you send them to the devnet. In this sense, devnet is related to the entire K framework.

Last updated: December 17, 2020 08:00 UTC