Runtime Verification has been recently awarded a research and development contract by IOHK to design a next generation virtual machine and a universal language framework to be used as core infrastructure for future blockchain technologies. The formal analysis and verification technology employed in this project has been developed and improved over more than 15 years of research and development, both in the Formal System Laboratory (FSL) at the University of Illinois at Urbana-Champaign and at Runtime Verification, with generous funding from organisations including NSF, NASA, DARPA, NSA, Boeing, Microsoft, Toyota, and Denso. It is about time that aircraft grade, software analysis technology used for mission critical software gets deployed to smart contracts, the blockchain and cryptocurrencies. The project will be executed by a team of Runtime Verification experts led by Prof. Rosu, who will work closely with students at the University of Illinois, also funded by IOHK, and with IOHK R&D personnel. IELE and K Team Photo, left to right: Daejun Park (PhD student at UIUC, RV intern); Theodoros Kasampalis (PhD student at UIUC, RV intern); Yi Zhang (PhD student at UIUC, RV intern); Traian Serbanuta (RV; screen, left bottom); Grigore Rosu (RV and UIUC; screen, center, taking the picture); Virgil Serbanuta (RV; screen, right bottom); David Young (RV); Brandon Moore (RV); Yiyi Wang (RV); Dwight Guth (RV). Also Chris Hathhorn (RV), who missed picture.
Runtime Verification, Inc. (RV) along with the Formal Systems Lab at the University of Illinois (FSL) are announcing a joint initiative targeting the full formalization of the Viper smart contract programming language, using the K Framework to create a full formal definition of this research-oriented smart contract programming language. We believe this effort will yield a number of useful tools and artifacts, and can lay the foundation for the future of principled and formally rigorous smart contract development.