The first Cardano smart contracts testnet launches today, the KEVM testnet, 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.
A smart contract allows you to exchange something of value - money, property, shares - by means of a software protocol. The terms of exchange are agreed upon by the parties involved in the same way as a traditional contract, and the contract is executed automatically on the blockchain.
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.
Our second Cardano testnet to launch will be IELE, which is a new virtual machine for Cardano. IELE will be launched in July and is a register-based virtual machine similar to LLVM with an unbounded number of registers, that supports unbounded integers. With IELE, developers can write, compile and execute smart contracts, with improved security and performance compared to the KEVM testnet.
For now, we recommend that developers use the Solidity language on both testnets. However, the vision is that eventually smart contracts will be written in high-level languages that translate to IELE, such as new languages like Plutus (being developed by IOHK), but also existing languages such as Java or Python, and then IELE-to-IELE translators ensure the resulting code is optimal.
K was developed by Runtime Verification in collaboration with Professor Grigore Rosu’s Formal Systems Laboratory at the University of Illinois at Urbana-Champaign during the past 15 years, and incorporates the state of the art in language design, semantics and formal methods. Read more about the K framework in this blog from Prof Rosu, founder of Runtime Verification. A blog about formal verification and what this means for smart contracts will follow soon.
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.
We look forward to receiving your valuable feedback about using the testnets which will help us make Cardano best in class.