Last week, Cardano (ADA) launched its first smart-contracts “KEVM” testnet. According to Cardano team, the KEVM testnet, which is correct by construction version of the Ethereum Virtual Machine (EVM) specified in the K framework, was built by Runtime Verification with the support of IOHK. Furthermore, It is the first time a complete formal semantics of the EVM have been produced. Cardano team believes that it is yet another step towards the creation of third-generation blockchains.
A smart contract facilitates the exchange of any object of value (property, stocks, money, etc.) using a software protocol. Similar to a traditional exchange, the terms are agreed upon by both parties involved in a deal, but automatically executed on the blockchain using smart contracts, when certain parameters are achieved. This is done by specifying the contract’s requisite properties in K, combining the contract with the KEVM specification, and then using the K framework to verify those properties.
Cardano’s second testnet, named IELE, will be launched in July. IELE is a register-based virtual machine similar to LLVM. IELE is designed to have an unbounded number of registers and supports unbounded integers. Using IELE, developers can write, compile, and execute smart contracts with improved performance and security, compared to the KEVM testnet.
Cardano has recommended developers to use Solidity language on both testnets for the time being. Eventually, Cardano aims to make provision for smart contracts to be written in high-level languages that translate to IELE, such as Plutus (being developed by IOHK), Python, and Java. To arrive at optimal code, there will be even IELE-to-IELE translators.
K was developed by Runtime Verification in collaboration with Professor Grigore Rosu’s Formal Systems Laboratory at the University of Illinois and incorporates the state of the art in language design, semantics and formal methods.
