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.