News

We don't like to brag, but we are collecting what other folks write about our work (reverse chronologically). If you would like to receive all the RV News on regular basis, please subscribe here.



Stake.Fish

"We are happy to announce that the Batch Deposit Contract has officially been audited by Runtime Verification. Specifically, we have worked closely with Daejun Park of Runtime Verification, who has previously conducted an end-to-end formal verification of the Ethereum 2.0 deposit smart contract, to conduct this audit. We want to thank the Runtime Verification team for being diligent, helpful, and extremely responsive throughout the engagement.”
Full post


Quantstamp News

"Quantstamp’s experience includes securing over 5 billion USD worth of digital assets and working with over 140 startups, foundations, and enterprises. Quantstamp chose to develop the Hedera Hashgraph stablecoin standard in the K framework because it is robust, extensible, and widely adopted amongst developers. The framework shortens development time, provides formal guarantees about the correctness of functions, removes the need to develop new tests, and creates a shared understanding amongst developers concerning the architecture and functionality of implemented stablecoins. When stablecoins follow a secure framework, the framework facilitates the integration of implemented stablecoins into other financial applications. This type of modularity is the ideal environment to encourage the development of a healthy stablecoin ecosystem for enterprises.”
Full post


PlatON Network

"It was a great experience to work with RV engineers and scientists on the Griskard proof. I was very impressed by the team's ability to tackle complicated concurrent scenarios and edge cases. I am happy to have RV as part of PlatON's grand plan. Moving forward, there are plenty of opportunities to engage again, namely around protocol modeling and formal verification of smart contracts.” - James Qu, CTO PlatON
Full post


IOHK

"IELE is one in every of my favorite initiatives. It’s unbelievable stuff, it’s actually thrilling and I feel it gonna open up an entire new dimension of the product and I all the time believed that. After the nice collapse of 2017 we had nice-to-have vs. must-have and that was within the nice-to-have column. Plutus, Marlowe and this stuff are within the must-have column." - Charles Hoskinson, CEO IOHK
Full article


NASA

"Runtime Verification’s solution is to apply its K Framework, which is a mathematically rigorous toolset that gives users the ability to design and implement programming languages from basic principles, and derive software analysis tools for them following a correct-by-construction methodology. These factors allow users of the K framework to ultimately verify their programs and systems for maximum assurance." - Illinois CS
Full post


Algorand Foundation

“We are delighted to support Runtime Verification’s grant application,” said Sean Lee, CEO of the Algorand Foundation. “We believe that creating a formal framework for Algorand Smart Contracts (ASC1s) will enable the creation of innovative, secure, and reliable DAPPs and DeFi solutions on the Algorand blockchain.” - Algorand Foundation
Full post


Tezos Foundation

"Runtime Verification designs formal models for high-value application domains, then uses the models to develop domain-specific products and services focused on correctness and security. Building off of its previous Tezos work, Runtime Verification will create a formal verification framework for Michelson by extending its existing unit testing framework to handle the case of symbolic unit tests. This project will help make it easier for developers of all backgrounds to deploy secure Tezos smart contracts." - Tezos Foundation
Full post


NASA

We propose a new verification method for software intended to be flown on unmanned aircraft systems that is both automatic and inexpensive. In Phase 1 we will focus on a class of errors in C programs called “undefined behavior” (UB) because this makes the method both easy to use and easy to compare with existing static analysis tools. - NASA SBIR
Grant description


Uniswap

"Formal specifications and proofs of method-level correctness for the smart contracts in the uniswap-v2-core repository (namely UniswapV2Pair and UniswapV2Factory) were produced using the act specification language and K framework. [...] Formal specifications for the contracts in uniswap-v2-core were written in the act specification language. These specifications are then compiled into reachability claims in the K language, and proved using the K framework prover against the bytecode produced by the build system in the uniswap-v2-core repository." - Dapp Labs
Full report


PlatON Network

"To say we are excited to engage with PlatON Networks is an understatement. We began conversations with their team in late 2019 about how and where our two companies could engage. Although we discussed various opportunities, including those related to writing and verifying programs written in web assembly (WASM), we eventually settled on protocol verification as a good place to start what will hopefully become a long-term collaboration and partnership." - Patrick MacKay, COO
Full post


Ethereum Trust Alliance

"Today we are very pleased to announce the formation of the Ethereum Trust Alliance (ETA). The ETA is a group of global blockchain security companies that are creating a security rating system for smart contracts to help users gain greater awareness of smart contract security and differentiate contracts which have gone through rigorous security checks. The founding members are MythX, Quantstamp, Runtime Verification, Sooho, SmartDec and ConsenSys Diligence." - Ethereum Trust Alliance
Full post


Tezos Foundation

"Runtime Verification is a company aimed at using runtime verification-based techniques to improve the safety, reliability, and correctness of software systems. The purpose of this grant is to develop a formal semantics and reference implementation of Michelson, a domain-specific language for Tezos smart contracts, in the K Framework. The K language is designed to make language definitions as readable as possible while still ensuring a K semantics has a precise mathematical meaning, and is supported by the tools of the K Framework. The Runtime Verification team will also publish documentation and interact with the wider Tezos developer community as part of this project." - Tezos Foundation
Full post


Web3 Foundation

"The design and implementation of bridges to all major blockchains is one of our highest priorities. [...] Currently, the only way to generate a Polkadot Runtime is by using Rust along with Parity-built tools. We would like to increase the language options for developers to write these Runtimes and recently released an RFP for the development of a tool to generate WebAssembly Runtimes from AssemblyScript." - Web3 Foundation
Full post


Elrond Network

"The Elrond research and development team will work closely with Runtime Verification to further develop the K framework and its capability to generate correct-by-construction Virtual Machines for the blockchain. Through the research and development initiative between Elrond and Runtime Verification we aim to take smart contracts to the next level, and to make the GO backend developed by Elrond for the K framework, open source and available to the wide public." - Elrond Network
Full post


Algorand Foundation

"To achieve even greater assurance about the Algorand protocol, and to make future design and validation of new protocols easier, we have chosen to enhance our mathematical proofs on paper with machine-checkable formal verification approaches. For this purpose, we engaged Runtime Verification, a company with deep verification expertise, to verify the correctness of the Algorand consensus protocol." - Algorand Foundation
Full post


Ethereum Foundation

"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." - Ethereum Foundation
Full post


Gnosis

"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." - Gnosis
Full post


Panvala

"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." - Panvala
Full post


Chicago INNO

"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." - Chicago INNO
Full post


Uniswap

"Uniswap liquidity pools are autonomous and use the Constant Product Market Maker (x*y=k). This model was formalized and the smart contract implementation passed a lightweight formal verification." - Uniswap
Full post


Maker

"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." - Maker
Full post


Cardano Foundation

"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." - Cardano Foundation
Full post


IOHK

"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." - IOHK
Full post


Ethereum Foundation

"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." - Ethereum Foundation
Full post


All News

2020-11-16 | Stake.Fish | Getting closer to launch: The stakefish Batch Deposit Contract audit is complete

2020-10-28 | Quantstamp Labs | Formally Verifying Hedera Hashgraph's Stablecoin Framework

2020-10-26 | PlatON Networks | Runtime Verification completes another successful engagement with PlatON Networks

2020-10-12 | New World Times | IOHK indicators contract with Runtime Verification

2020-10-08 | Illinois CS | Rosu sharpens company vision with third NASA SBIR grant

2020-07-30 | Illinois CS | Sha models a more certain way forward for medical treatments during COVID-19 pandemic

2020-07-29 | Algorand Foundation | Runtime Verification Inc are the latest recipient of an Algorand Foundation Grant

2020-07-23 | Tezos Foundation | Announcing Fourth Cohort of Tezos Ecosystem Grants

2020-06-29 | NASA | A Semantics-Based Verification Toolset for UAS Embedded Software

2020-05-24 | Top 10 Blockchain Security and Smart Contract Audit Companies

2020-04-20 | Uniswap | Uniswap V2 Audit Report

2020-03-09 | CryptoNinjas | Runtime Verification enters a protocol verification agreement with PlatON blockchain

2020-03-09 | PlatON Networks | Runtime Verification Enters a Protocol Verification Agreement with PlatON

2020-02-04 | Ethereum Blog | Audit and formal verification of deposit contract bytecode completed by Runtime Verification

2020-02-03 | ETA | Runtime Verification joins Ethereum Trust Alliance (ETA) as a founding partner

2020-01-29 | 6 Best Smart Contract Auditors For Blockchain Platforms

2019-09-10 | Tezos Foundation | Announcing Second Cohort of Tezos Ecosystem Grants

2019-08-17 | Web3 Foundation | Web3 Foundation Grants — Wave 3 Recipients

2019-07-14 | Elrond Network | Elrond Initiates Cooperation With Runtime Verification — A Research and Development Company Specializing in Formal Methods

2019-06-25 | Algorand | Runtime Verification Formally Verifies the Algorand Blockchain Will Never Fork

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-10-12 | Uniswap | Lightweight Formal Verification of Uniswap Smart Contract

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