Cardano Smart Contracts Testnet Release


IOHK is pleased to announce the release of the KEVM testnet. This is the first smart contracts testnet for Cardano. Smart contracts must be formally verified, so they run exactly as specified and are free from bugs or flaws. Only then can they be widely adopted as financial infrastructure that can be relied upon by billions of people.

The KEVM is a correct by construction version of the Ethereum Virtual Machine (EVM) specified in the K framework. This technology, produced by Runtime Verification with the support of IOHK, is the first time that a complete formal semantics of the EVM have been produced. This is an important first in cryptocurrency that is a necessary step towards the promise of third-generation blockchains.

Developers will be able to take any application that runs on the EVM and execute it on the KEVM, which can also be used to rigorously prove that smart contracts work correctly. This is done by formally 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.

Read the full statement and watch our video introducing the Cardano testnets.


24.05.2018 - Summary of Charles Hoskinson's Video Update

For lazy people, here it is :slight_smile:


Great stuff!


I cant request Fauce, the following error appears:

An unknown error has occurred. This may be due to an unknown address or component-related error.

Please confirm the address you are using is correct.

If you need to raise an issue please refer to support


Hi! I think it would be more suitable to ask about troubles like this in our dev chat :slight_smile: Might get faster response there.


Good information. Thanks, Laurie!


Is there any tutorial/intro how to actually verify a EVM smart contract and how to deploy it to the Cordano testnet?


I’m not sure what you mean by “verify”, but you can find useful info in the “Get Started” section:


The main new idea, in my understanding, for this release is that the KEVM is used. From the website:

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.

I was wondering if there are examples or tutorials to verify a Solidity smart contract using the K framework and how to use the wallet to deploy the contract to the testnet.


Hi yanik, please head over to: and submit a ticket. Thanks for your feedback!


I am Janis Ratkevics. I working in ministry of Environment protection and regional development of Republic of Latvia. We discuss about possibilities to make regulation for smart contracts. We are interested in some private company, who can make a technological platform for smart contracts. If you are interested in, please contact me at