Next-Generation Virtual Machine Sets Future Standard of Blockchain Development

New York, New York - October 24, 2024 - Runtime Verification, a University of Illinois startup founded by computer science professor Grigore Rosu, and IOHK, a leading blockchain research and development company, are partnering to design a next-generation virtual machine called IELE and a universal language framework to be used as core infrastructure for future blockchain technologies. The proposed technology, which is based on formal methods and state-of-the-art programming language theory, will bring much greater security and dependability to blockchain systems and will reduce the risk of vulnerabilities that can lead to hacks.

The project, which is funded by IOHK, will be executed by a team of experts led by Prof. Rosu, who will work closely with students at the University of Illinois and the IOHK research and development team.

Prof. Rosu, CEO of Runtime Verification, said: “We are very excited to pursue this new project with IOHK. It is about time that an aircraft grade software analysis technology that has so far been used in the context of mission critical software gets deployed to smart contracts, the blockchain and cryptocurrencies.”

The techniques used in this project have been developed over the last 15 years with funding from organizations including NSF, Nasa, Darpa, NSA, Boeing, Toyota, Samsung and Microsoft, at the Formal System Laboratory at the University of Illinois at Urbana-Champaign and by Runtime Verification.

“Mathematical rigor and good design of programming languages and underlying virtual machines are critical for the success of blockchain technologies and applications. Indeed, decades of accumulated evidence show that formal techniques and their early adoption in the design of computing systems can significantly increase safety, security, and dependability of such systems,” said Prof. Rosu.

“Moreover, when paired with good user interfaces that hide the mathematical complexity, such techniques can also increase the effectiveness, elegance, and quality of code development; a good example in this direction is the recent success of functional programming languages and of automated theorem provers or constraint solvers.”

The research also aims to enable developers to write secure smart contracts in any programming language that has formal semantics in K, such as C, Java, JavaScript, Solidity, Plutus, and many more. The project also includes plans to develop a concrete execution backend to K that will be at least one order of magnitude faster than the current one.

Charles Hoskinson, CEO of IOHK, said: “I’m honored and humbled to work with Grigore and his team at Runtime Verification on bringing both the K Framework and semantics based compilation into the cryptocurrency space. These innovations alongside Cardano’s new virtual machine - IELE - will eventually enable developers to write smart contracts in the programming language of their choice and with the tools they have come to know and love. Furthermore, we are extremely excited to explore formal verification of smart contracts with the RV team in order to ensure higher security, performance and reliability as smart contracts begin to pivot from experiments to enterprise and government adoption.”

About IOHK:

Founded in 2015 by Charles Hoskinson and Jeremy Wood, IOHK is a technology company committed to using peer-to-peer innovations to provide financial services to the three billion people who don’t have them.

IOHK is an engineering company that builds cryptocurrencies and blockchains for academic institutions, government entities and corporations. It is also a research firm with dense academic connections in Europe, America and Asia with many employees holding PhDs in Computer Science, Math or Physics. IOHK focuses on practical, peer reviewed research to create live protocols, and the technological underpinnings to next-generation cryptocurrencies.

To learn more, visit iohk.io