IELE is an improvement on the Ethereum blockchain virtual machine (EVM). It was created after the KEVM project demonstrated that a K formal specification of EVM could automatically generate a VM comparable in performance to hand-crafted implementations.
IELE's follow-on goals were to:
Automatically generate a virtual machine competitive in speed with a hand-crafted VM. The trick is to make the low-level bytecode language similar to that of LLVM, a proven compiler toolkit used in (for example) Apple's compilers.
Remove opportunities for exploits of buggy smart contracts. For example, arithmetic overflow cannot be exploited if integers grow as needed instead of overflowing. And EVM's small, fixed-size runtime stack can be exploited; IELE's grows as needed and can't be.
Support the Solidity blockchain language as well as upcoming languages like Vyper, Plutus, and, perhaps, JavaScript.
Have a gas model that better captures a contract's use of resources. For example, a variable containing the small integer5 is cheaper in IELE than in EVM because you pay for one machine word instead of four. If your integer grows very large, though, you'll pay for all the machine words it requires.
Have a more readable low-level language than EVM has. In the final analysis, the bytecodes on the blockchain are the smart contract that gets executed. Analysis of a contract as written in Solidity has a chain-of-custody problem: how sure are you that a particular Solidity contract produced the bytecodes on the blockchain? The suspicious user will audit at the bytecode level.
Proofs of correctness are already tractable for EVM contracts (at the bytecode level); a goal for IELE was to make them easier. For example, proofs needn't concern themselves with arithmetic overflow because arithmetic overflow is impossible. IELE's register-based VM (instead of EVM's stack-based one) requires less busywork in the proof.
Except for the speed goal (where the work is ongoing), these goals have been achieved, and IELE has been successfully deployed to the Cardano testnet.
IELE is open source, so its specification and supporting documentation are available on GitHub.
