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.

© IOHK 2015 - 2021


Cardano is an open-source project.

Cardano is a software platform ONLY and does not conduct any independent diligence on, or substantive review of, any blockchain asset, digital currency, cryptocurrency or associated funds. You are fully and solely responsible for evaluating your investments, for determining whether you will exchange blockchain assets based on your own judgement, and for all your decisions as to whether to exchange blockchain assets with Cardano. In many cases, blockchain assets you exchange on the basis of your research may not increase in value, and may decrease in value. Similarly, blockchain assets you exchange on the basis of your research may fall or rise in value after your exchange.

Past performance is not indicative of future results. Any investment in blockchain assets involves the risk of loss of part or all of your investment. The value of the blockchain assets you exchange is subject to market and other investment risks