Virtual Machines

Formal Design, Implementation, and Verification of Blockchain Languages

In this conference, Grigore Rosu, founder of Runtime Verification, explains that many of the recent cryptocurrency bugs and exploits are due to flaws or weaknesses in the underlying blockchain programming languages or virtual machines.

The post-mortem approach to formal language semantics and verification, where the language is implemented and used in production for many years before the need for formal semantics and verification tools arises, simply does not work anymore.

New blockchain languages and virtual machines are being proposed at an alarming rate, followed by new versions of each of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially large value.

Formal analysis and verification tools are therefore needed immediately for these languages and virtual machines. At Runtime Verification we use recent academic and commercial results to develop blockchain languages and virtual machines that come equipped with formal analysis and verification tools from the outset. The idea is to generate all of these automatically, so that they are ‘correct by construction’ from a formal specification. We demonstrate the feasibility of this approach by applying it to two blockchains, Ethereum and Cardano.

© 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