Runtime Verification & IELE – from interoperability to universality

Professor Grigore Rosu, President and CEO of start-up Runtime Verification (RV) joined us on March's edition of the Cardano360 show to share ideas and discuss the collaboration between RV and IOHK.

Our professional relationship with Grigore and RV started back in 2017, and Grigore’s credentials speak for themselves (in any language). He’s worked for NASA, DARPA, Microsoft, and has taught at the University of Illinois Urbana-Champaign, to name but a few achievements.

Grigore is also credited with the creation of the K Framework, which has been described as ‘software that simply cannot afford to fail.' Developed over 15 years, the framework’s primary purpose is to enhance security. We’ll get into this in more detail later, but first, a short history lesson.

When it comes to smart contracts, the Ethereum Virtual Machine (EVM) set many early standards, for example the creation of the ubiquitous ERC-20 smart contracts, written in Solidity. However, this system isn’t flawless. Smart contracts have known coding vulnerabilities that have caused security issues. 

IELE: Unparalleled security, scalability, and programmability

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

IELE takes things a step further. As discussed by Rosu on March’s Cardano360 show, IELE (named after a faerie-like creature of Romanian myth) is a virtual machine that executes smart contracts, and also provides a human-readable language for blockchain developers. IELE was designed with formal methods in mind to address security and correctness concerns inherent in writing Solidity smart contracts targeting Ethereum, easing the path to heightened levels of security, scalability, and programmability. 

IELE resembles the intermediate representation of the LLVM compiler. This enables drawing on the wealth of knowledge available in the LLVM community, specifically, the work that has gone into writing safe and effective compiler optimization passes over LLVM IR. Much of the effort put into the LLVM compiler can be ported to the IELE optimizer as well.

About LLVM

When IELE is implemented (Rosu indicated that an initial proof of concept would be available for testing around six months from now), the opportunity for development will be even wider. IELE operates more like a passport than a virtual machine, opening the doors – if not the floodgates – to a wealth of new and unique talent. Some developers may have once dismissed the idea of entering the blockchain space, as it would likely have meant learning an entirely new programming language. As a direct result of RV’s innovative approach, any developer wanting to get involved in smart contracts can write them in a language they are comfortable with, including Solidity. The resulting output would run successfully on any IELE-powered blockchain, irrespective of the source language.

What does this mean for Cardano?

This achievement will offer developers and businesses yet another incentive to migrate from Ethereum and participate in the Cardano blockchain. Openness, inclusivity, and interoperability are the foundations upon which Cardano was built. Our philosophy is – and always has been – to welcome developers from all backgrounds, to ensure Cardano’s steady evolution. Rosu has bold plans. 'IELE is the crown jewel of our research over the past decade,' he says. 'It’s the maximum you can hope for on a universal framework.'

Final thoughts

IOHK’s partnership with RV demonstrates a commitment to innovation, and to opening Cardano to as wide a development community as possible. The KEVM/IELE implementation will expand Cardano’s reach and interoperability by creating novel avenues of cooperation that will lead to the exploration of new ideas, concepts, and technological developments in the context of a ‘correct by construction’ environment. 

You can read more from Alex at Cardano community site Adapulse.