News

We don't like to brag, but we are collecting what other folks write about our work (reverse chronologically):



"Many resources are shifting into testing, fuzzing, and audits over the coming months. We engaged Runtime Verification to formally verify the deposit contract and to formally specify the Beacon Chain. This is in addition to considerable effort by the research, development, and security teams involved in ETH 2.0 toward reliability and security."
Full post


"Our team worked closely with Runtime Verification (RV) — a company that specializes in using runtime verification techniques to ensure that software systems are secure — to release a formal verification report. While testing and auditing are essential steps in the development process, formal verification is a mathematical proof-based methodology used to significantly decrease the likelihood that a smart contract is buggy."
Full post


"Runtime Verification has been working closely with Rikard Hjort of Chalmers University on the KWasm semantics, which will allow Web Assembly contracts to be formally verified using the K framework. The core computational opcodes are finished, what remains are memories, tables, and modules. Memories are almost done, awaiting final review and approval, and tables will follow shortly."
Full post


"Runtime Verification, based in Urbana, has developed tools to improve the safety and reliability of software systems. Its technology can automatically detect bugs that are lurking in a company’s software, and identify problems before a program crashes. Runtime’s customers include a handful of high-profile clients—such as Boeing, NASA, Toyota and the National Science Foundation—who use the startup to make sure their code is error free. For these types of companies, if their software fails, the stakes are higher than, say, a shopping app or a dating website. Detecting problems as soon as possible helps machines run better and keeps people inside those machines safer."
Full post


"To provide the highest confidence that the contracts behave as expected, we are working with Runtime Verification to provide us with a formal and mathematically provable audit of the Multi-Collateral smart contracts. We believe MakerDAO will be the first production smart contract system that is formally verified in this manner."
Full post


"The K framework was used to formally model the semantics of the Ethereum Virtual Machine, and the knowledge gained from this process was employed to design IELE, the virtual machine for Cardano that will be released in a test format in a few weeks’ time. This is the first time this technology has been deployed within the blockchain industry. Importantly, K is a means to formally verify the code of smart contracts, so they can be automatically checked for the types of flaws that have led to catastrophic financial loss, and must be avoided at all costs."
Full post


"The first Cardano smart contracts testnet launches today, the KEVM testnet, a correct by construction version of the Ethereum Virtual Machine (EVM) specified in the K framework. This technology, produced by Runtime Verification with the support of IOHK, is the first time that a complete formal semantics of the EVM have been produced. This is an important first in cryptocurrency that is a necessary step towards the promise of third-generation blockchains."
Full post


"These grants will fuel the teams working hard at research & development to support the entire ecosystem. Furthermore, we hope that these grants will signal to the community what we think are the missing pieces in the ecosystem that need more support. Said in another way, the Foundation is here to serve teams and individuals that are working to prevent a tragedy of the commons."
Full post


All News

2019-05-21 | Ethereum Foundation | Ethereum Foundation Spring 2019 Update

2019-05-05 | Waves | Mathematically proven 100% safe smart contracts

2019-04-27 | Week in Ethereum News | Gnosis Safe gets formally verified by Runtime Verification

2019-04-26 | Gnosis | Formal Verification— A Journey Deep into the Gnosis Safe Smart Contracts

2019-04-23 | UIUC CS News | Bootstrapping in Chicago

2019-04-03 | Panvala | Batch Two Token Grant Applications

2019-03-27 | Elrond Network | Welcoming Grigore Rosu as Advisor to Elrond

2019-01-04 | UIUC Research Park | EnterpriseWorks Graduate Runtime Verification Thrives in Urbana

2019-01-03 | Chicago INNO | Meet the IL Startup Helping NASA and Boeing Detect Errors in Their Software

2018-11-30 | Gnosis | Formal Verification of the Gnosis Safe Contracts

2018-10-18 | Bitrates | MakerDAO: A Stability Engine With a Decentralized Governance Model

2018-09-17 | MakerDAO | The Code is Ready

2018-08-22 | MakerDAO | Update on Availability of Multi-Collateral Dai

2018-08-21 | CASA | Storing your Ethereum Safely

2018-08-09 | Week in Ethereum News | Runtime Verification: how formal verification of smart contracts works

2018-08-01 | Cardano Forum | Webcast with Grigore Roșu, CEO of Runtime Verification

2018-07-31 | BC Focus | IOHK launches Cardano smart contracts testnet for IELE virtual machine

2018-07-31 | Crypto Ground | IOHK Launches Second Cardano Smart Contracts Testnet 'IELE'

2018-07-30 | Payment Week | IOHK Launches IELE Virtual Machine Testnet for Cardano Blockchain

2018-06-14 | Blokt | Cardano Brings Forward Its First Smart Contracts

2018-06-12 | Crypto News Monitor | Grigore Rosu: The K framework – a framework to formally define all programming languages

2018-06-07 | Bitrates | IOHK: Virtual Machines and Contract Code Correctness

2018-06-05 | invest in blockchain | Cardano Launches KEVM Testnet: What This Means and Why This is a Big Deal

2018-05-28 | IOHK | First Cardano smart contracts testnet launches

2018-03-07 | Ethereum Foundation | Announcing Beneficiaries of the Ethereum Foundation Grants

2017-12-20 | All Coins News | Virtual Machine for Blockchain Launched by Runtime Verification and IOHK

2017-12-20 | Chain Finance | Virtual Machine for Blockchain Launched by Runtime Verification and IOHK

2017-12-18 | Payment Week | Runtime Verification and IOHK Launch Virtual Machine for Blockchains

2017-12-18 | Payments Journal | Runtime Verification and IOHK Launch Virtual Machine for Blockchains

2017-12-18 | UIUC CS News | Runtime Verification and IOHK Launch Virtual Machine for Blockchains

2017-10-03 | UIUC CS News | Student uses a tool called K to build a path towards more secure blockchains

2017-10-02 | Crypto Ninjas | Research project produces first complete formal semantics of the Ethereum Virtual Machine

2017-08-02 | Econo Times | IOHK’s UIUC project builds formal semantics of Ethereum Virtual Machine

2017-08-02 | Coin Journal | KEVM Wins IC3-Ethereum Crypto Boot Camp 2017 Competition

2017-08-01 | Coinspeaker | IOHK-Funded UIUC Project Produces First Complete Formal Semantics of Ethereum Virtual Machine

2016-10-31 | UC San Diego | CSE Alumnus Wins Most Influential Paper for Work on Runtime Verification

2016-10-17 | UIUC CS News | Rosu earns ASE Most Influential Paper award for work that helped launch runtime verification field