4 min readOct 19, 2021

IELE is a virtual machine that executes and verifies smart contracts, and also provides a human-readable language, geared towards blockchain developers.

IELE was designed using formal methods to address the security and correctness concerns inherent in writing Solidity smart contracts on Ethereum. When a smart contract is written in IELE, it is more secure and it is easier to verify its correctness. It benefits from an easy-to-use and readable language structure, and overall performance improves.

The Ethereum Virtual Machine (EVM) was the first to be deployed in a network blockchain. This is why many refer to Ethereum, as the chain of computing blocks; was the first to allow programmers to run calculations on the blockchain.

This, at the time, was opposed to Bitcoin, which can only store transaction data (essentially read / write). The approach was a milestone in the blockchain space, and it also has very good capabilities: it is turing-complete (140 opcodes, or machine commands, are available to the VM) , it has an intermediate language compiler that converts Solidity to opcodes.

The problem, however, is that although EVM is turing-complete by definition, it is not by execution, and that is because of gas rates. The EVM introduced a novel approach to keeping the decentralized network self-sufficient called gas. Every time a smart contract wants to execute some machine code, it needs to have a gas balance provided by the issuer.

The problem, as many have experienced, is that while the EVM may be turing-complete by definition, it is limited by the available gas provided to the smart contract. In essence, it can only do what it is allowed to do, which prevents true full turing.

A Turing machine is a device that manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can be adapted to simulate the logic of any computer algorithm and is particularly useful in explaining the functions of a CPU within a computer. In the theory of real and virtual computers, programming languages, and other logical systems, a complete Turing system is one that has computational power equivalent to the universal Turing machine. In other words, the system and the universal Turing machine can emulate each other.

Since late 2020, Cardano developers have bridged the Solidity / Ethereum community through the Ethereum K Virtual Machine (KEVM), an implementation of the EVM specified in the K framework, which enables developers to use the formal verification tools that K produces to check the correctness of a contract.

The K framework is what is known as a semantic framework programming language. It means that you mathematically formalize, rigorously, the programming language, once, and then that mathematical artifact automatically, or semi-automatically, derives all the tools that are needed for that language.

IELE started a while ago, it was when Runtime Verification (the developer company), was making the initial commitments to IOHK in 2018. IELE actually started as a design language, so it was easier to reason with than EVM. IELE now needs to be updated and that is why it is working on its update, to reach the point of a stable state as with the KEVM.

IELE, (named after a fairy-like creature from a Romanian myth) , goes one step further. It is a virtual machine that executes smart contracts and also provides a human-readable language, and aimed at blockchain developers . IELE was designed with formal methods in mind to address the security and propriety concerns inherent in programming Solidity smart contracts targeting Ethereum, thus paving the way to high levels of security, scalability, and programmability.

IELE bears a resemblance to the intermediate representation of the LLVM compiler. This allows you to take advantage of the wealth of knowledge available in the LLVM community, specifically, the work that has gone into programming safe and efficient compiler optimization goes beyond LLVM IR. Much of the effort put into the LLVM compiler can also be carried over to the IELE optimizer.

The IELE development network provides better performance and is log-based, which means that it can make use of a wider range of analyzes and optimizations than a stack-based virtual machine such as KEVM. This enables more accurate gas cost predictions to be made, as well as reducing the cost of gas in contracts.

Debugging contracts is easier, because IELE has a different status error code for each of the exceptions that can occur while functions within a contract are executing.

Some developers might have rejected at some point, the idea of ​​entering the blockchain space, as this would likely have meant learning a completely new programming language. As a direct result of Runtime Verification’s innovative approach, any developer who wants to get involved in smart contracts can program them in whatever language they are comfortable with, including Solidity. The resulting output would run correctly on any blockchain that supports IELE, regardless of the source language.

When IELE is implemented, the development opportunity will be even broader. IELE operates more like a passport than a virtual machine, opening the doors to a host of new and unique talents.

This achievement will offer developers and companies another additional incentive to migrate from Ethereum and participate in the Cardano blockchain . Openness, inclusiveness, and interoperability are the foundations on which Cardano was built.




Researcher • ϚʁyptøWriter • Content Creator | 𝕏 @liberlion17 | nostr | website: