IOHK, the engineering company developing the Cardano blockchain announced that the first Cardano smart contracts testnet launched 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 has been produced.
Gerard Moroney, Project Manager at IOHK said, “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 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.
The 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, the IOHK team recommends 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.
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.
