Cardano Launches Testnet – its First Smart Contracts
IOHK is an engineering company behind the development of Cardano blockchain. The most recent development concerning Cardano is that it launched its first smart contracts testnet. The testnet, called KEVM, is a correct by construction version of the Ethereum Virtual Machine (EVM) that is apparent in the K framework. The framework was developed by Runtime Verification with IOHK’s support and it is the first time EVM’s complete formal semantics has been development.
IOHK’s project manager Gerard Moroney stated, “this is an important first in cryptocurrency that is a necessary step towards the promise of third-generation blockchains.” For those who are still uncertain about the meaning of smart contract, it is essentially a contract that users can exchange for something of value, such as property, money, and shares. The exchange is facilitated by a software protocol. The parties agree upon the terms of the exchange similar to that of a traditional contract and the contract is also automatically executed on the blockchain.
The developers behind the system can expect to take an application running on the EVM and to execute it on the KEVM. This process makes it easier for them to prove that the smart contracts function properly. Further, the process is facilitated by formally specifying a contract’s desired properties in the K and by combination of the contract with KEVM specifications. The final step is where the K framework verifies the properties.
At this point, the IOHK team recommends solidify language be applied by developers on both testnet. It is also important to note that the company’s vision is have the smart contracts written in high-languages that translate to IELE. The main languages include Plutus, which is being developed by IOHK, and existing languages like Java and Python. At the end of the process, the IELE-to-IELE translators will ensure that the resulting code is optimal.
For those who are unware, Runtime Verification and its collaboration with Professor Grigore of Rosu’s Formal Systems Laboratory at the University of Illinois at Urbana-Champaign developed K over the course of 15 years. The system incorporates the state of the art language design, semantics, and formal methods.
Further, smart contracts require formal verification so that they run exactly as specified and are free from flaws, bugs, and other issues. When they meet such specifications, the contracts can be adopted on a widescale basis as financial infrastructure the people can rely upon.