Virtual Machines

K framework for Cardano and IELE

In this video, Grigore Rosu describes his research and work with IOHK since June 2017 to develop technology based on formal semantics for Cardano, including a virtual machine. Grigore is professor of computer science at the University of Illinois at Urbana-Champaign, and chief executive of the start-up company, Runtime Verification.

The K framework has been developed by Grigore and Runtime Verification over 15 years. It is used in mission-critical applications – this is software that cannot afford to fail. To this end, Runtime Verification has worked with companies including Nasa, Boeing, and Toyota. His collaboration with IOHK began after he was contacted by Charles Hoskinson. The IOHK chief executive had spotted that the software vulnerabilities that had resulted in many hacks on blockchains and the draining of cryptocurrencies worth hundreds of millions of dollars, could have been prevented using the formal methods developed by Runtime Verification.

© IOHK 2015 - 2021


Cardano is an open-source project.

Cardano is a software platform ONLY and does not conduct any independent diligence on, or substantive review of, any blockchain asset, digital currency, cryptocurrency or associated funds. You are fully and solely responsible for evaluating your investments, for determining whether you will exchange blockchain assets based on your own judgement, and for all your decisions as to whether to exchange blockchain assets with Cardano. In many cases, blockchain assets you exchange on the basis of your research may not increase in value, and may decrease in value. Similarly, blockchain assets you exchange on the basis of your research may fall or rise in value after your exchange.

Past performance is not indicative of future results. Any investment in blockchain assets involves the risk of loss of part or all of your investment. The value of the blockchain assets you exchange is subject to market and other investment risks