Runtime Verification

Category: News

What we announced, and underneath it what other people wrote about us.

Hardening Linux's C Code: A Rewrite-and-Verify Loop

By Natalie KlausAugust 20th, 2026

While testing our reusable C-to-Rust verification workflow on the Linux UVC parser, we found a real integer-overflow bug and joined the upstream fix. The workflow combines a safe Rust rewrite, differential fuzzing against the kernel C, and Lean proofs of the key safety properties behind CVE-2024-53104.

Off site

Runtime Verification and Assurea Partner to Strengthen Software Safety for Medical Devices, SaMD and Artificial Organs

By Runtime VerificationAugust 18th, 2026

Runtime Verification and Assurea Partner to Strengthen Software Safety for Medical Devices, SaMD and Artificial Organs

Verifying Linux's Rust Code: From Binder To Lean 4

By Natalie KlausAugust 5th, 2026

Android's Binder driver parses attacker-controlled bytes on three billion devices. As part of our formal verification work targeting Linux kernel, we proved that its deserializer never panics on any userspace input, all machine-checked end-to-end from production Rust through Charon and Aeneas into Lean 4.

The Engineered Chaos Bugs Fear

By Runtime VerificationJune 15th, 2026

Fuzzing is one of the most practical ways to find bugs that unit tests miss, especially in large code bases. At a basic level, a fuzzer repeatedly feeds a series of not-so-randomized inputs into a program with the objective of identifying crashes, failed assertions, unexpected behavior, or broken assumptions. Many modern languages now have good fuzzing support built into or near the standard developer workflow.

The Future of Safety for Software as a Medical Device (SaMD)

By Runtime VerificationJune 11th, 2026

A simple bug in the software running inside a pacemaker or an insulin pump is not just a crashed app but it could also put thousands of lives at risk. Software as a Medical Device has raised the stakes of every line of code, and the testing toolkit alone is no longer enough.

When the Software Holds but the Money Leaves Anyway

By Runtime VerificationJune 3rd, 2026

A technical analysis of the April 2026 KelpDAO bridge incident, in which $292M was lost despite every audited on-chain component performing exactly as specified, with the actual compromise occurring in the off-chain operational layer that surrounded them.

What the TanStack npm compromise tells us about software trust.

By Runtime VerificationMay 20th, 2026

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

From Rust Code to Mathematical Proof: How We Verify Safety-Critical Rust

By Natalie KlausMay 19th, 2026

Runtime Verification applies formal methods to cryptographic and safety-critical software. We turn production Rust into machine-checked Lean 4 proofs of correctness, no sorry left behind.

The risk of open source code: what the past still teaches us

By Runtime VerificationMay 18th, 2026

The most consequential security failures in privacy software rarely come from anyone being careless. They come from properties that held in one place and quietly stopped holding in another.

How a single unit difference caused a $370 million space disaster

By Runtime VerificationMay 7th, 2026

Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.

AI is making software harder to secure

By Runtime VerificationMay 5th, 2026

Last week was a bad one for tech companies. Vercel got breached through a third-party AI tool with too much access. Bitwarden shipped a backdoor through a compromised dependency. At Lovable, any user could read any other user's project. And $292M left KelpDAO after a single outside verifier got compromised and signed a forged message.

KelpDAO Audit Passed. $292M Left Anyway.

By Runtime VerificationApril 20th, 2026

On April 18, 2026, an attacker drained $292M from KelpDAO's Ethereum escrow in a single transaction. The OFTAdapter contract that released 116,500 rsETH did exactly what it was designed to do. No bug was exploited, no zero-day in LayerZero's on-chain code. The entire on-chain system was, by conventional security standards, clean.

In their words

Partners, investors and grant committees, on the record.

An archive, not a feed. Nothing below has been added since June 2021; anything newer is in the posts above, and is mirrored to Medium. It is kept for the record.

Runtime Verification logo
“I am very pleased that our investors have embraced our unique language-parametric approach, built over more than 20 years within the K Framework. The generality of our approach allows our tools to be easily configured to work with different programming languages and different blockchains. The fact that five blockchains joined our investment round through their funds, based on research from their development teams who witnessed our technology, is a testament to the universality and strength of our K-powered technology.”

Grigore Rosu, Founder and CEO Runtime Verification

Full post
IOSG logo
“As someone who was fighting cybersecurity risks on a daily basis, I’d always been looking for the “ultimate” solution to the arms race between the adversaries and the defenders, until I met with formal verification. It completely shifts the paradigm from looking for potential loopholes to certifying a software program is correct and thus “bug-free”. It is the “holy grail” of software security. Runtime Verification is a cross-industry leader in the quest to such “holy grail”. By carefully designing technology, framework, and tools to apply the mathematical rigor to software programs, it has made formal verification ever more practical. Critical software and infrastructure in the aerospace and automobile industries has been benefiting from it in the past decade. Now with the thriving decentralized economy, Runtime Verification has applied their technology to safeguarding some of our most frequently used blockchain infrastructures and applications as well. We are truly excited to work closely with Runtime Verification and embark on the next journey to take formal verification to our everyday software systems.”

Xinshu Dong, Partner IOSG Ventures

Full post
Maven 11 logo
“Security is key for DeFi to mature even further. We cannot expect this to grow to a trillion dollar industry without institutional grade security. Runtime Verification provides exactly that. By using formal verification they go a step further than other audits and provide security while working alongside teams. We are excited to kick off the next growth phase for the company.”

Balder Bomans, Managing Partner Maven 11 Capital

Full post
MultiversX network logo
“We are excited about being able to secure a voice for the MultiversX Network at the heart of developing what we believe to be essential tools for the advancement of the general blockchain space. Our strategic investment in Runtime Verification aims for the sustainable growth of methodologies and devkits that already are embedded into the core practices involved in building the MultiversX protocol and connected tools.”

Beniamin Mincu, CEO MultiversX Network

Full post
MultiversX network logo
“After several months of working together, we already were able to create a K-Framework replica of our Arwen VM dubbed KArwen. Arwen is a WASM VM so Runtime Verification was able to expand their KWasm semantics for WASM to accommodate our virtual machine. The resulting KArwen is a fully formalized auto-generated virtual machine that can execute MultiversX Smart contracts. This lays the groundwork for advanced formal tooling to be used for the MultiversX smart contracts. An important outcome is also that Mandos testing using the K Framework already allows developers to perform code coverage testing at a lower level than previously possible.”

MultiversX

Full post
IOHK
“Mantis will also use Runtime Verification’s ‘K’ framework to give more sophisticated techniques for smart contracts verification and more predictable gas costs, making the platform more appealing, both to developers building smart contracts and end users looking for a cost-effective secure blockchain platform.”
Full post
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 blockchain logo
“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 post
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
Web 3 Foundation logo
“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
MultiversX network logo
“The MultiversX 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 MultiversX and Runtime Verification we aim to take smart contracts to the next level, and to make the GO backend developed by MultiversX for the K framework, open source and available to the wide public.”

MultiversX Network

Full post
Algorand blockchain logo
“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

In the press

Every mention we collected between 2016 and 2021.

2021

2020

2019

2018

2017

Have critical software that has to be right? Let's talk.

Get in touch
10+
Years in formal methods
NASA & Boeing
Early heritage, before blockchain
Trusted
By leading blockchain foundations