Category: news
Verifying Linux's Rust Code: From Binder To Lean 4
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
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)
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
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.
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
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
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
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
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.
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.
Wonderland CTF 2026: Fixed Deposits Challenge Results by Runtime Verification
Earlier this week, our team at Runtime Verification participated in Wonderland’s CTF, providing one of the challenges to snatch a piece of the $30,000 prize pool. We want to thank everyone who joined us and worked tirelessly to solve all the challenges (and congrats to the winning teams!).
Introducing the Simbolik Contributor Program
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Simbolik Expands into a Full Security Toolkit for Solidity Engineers
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
The RV Ethos
It's not for some effort towards external transparency, but rather to provide inspiration for those out there that might think "there must be a better way to do business with each other!". If this story of sustainability, transparency, and ultimately decentralization excites you, you might be one of those in the space that maintains a similar ethos to us.
Meet the RV Team at DevCon
Our team is already in Thailand, ready to take over DevCon and the side events organized by different teams in the ecosystem! In this blog, we list all the events where our team will be speaking, how to get in touch with us and meet us, and update you on the latest developments in our tooling.
K 7.0: Improving K for Ecosystem Tool Developers
April 2024 saw the release of version 7.0 of the K Framework. Previously, K was focused on the implementation of programming language semantics, and external tool support was required to expand those semantics into production tooling for a language. In K 7.0, we have merged our Python support library for K (Pyk) into the K compiler, making it the primary way for tool developers to interact with K.
Runtime Verification Hosts EthCluj Workshop on Formal Methods
On April 14th, Andrej Vacaru and Raoul Schaffranek from Runtime Verification were privileged to lead an online workshop hosted by the EthCluj community. We are sincerely grateful for this opportunity, which allowed us to share our passion for innovative software verification tools with an engaged audience.
Runtime Verification Launches a Registered Algorand Relay Node
We are thrilled to announce that Runtime Verification has launched a new registered Algorand relay node, contributing to the operation of Algorand’s network
Runtime Verification Brings Formal Verification to Algorand
We are happy to announce the public beta of KAVM — the formal semantics of the Algorand Virtual Machine built with the K framework!!
Runtime Verification Audits World Mobile EarthNode NFT Claiming Contract
Runtime Verification is proud to announce the successful completion of its audit of the World Mobile EarthNode NFT claiming contract. World Mobile is a blockchain-based mobile network aiming to connect people and communities globally. The audit examined the EarthNode NFT claiming smart contract, which manages NFT ownership for node operators, who can earn rewards in the form of the native WMT currency by contributing to the sharing economy. After a comprehensive manual code review, the audit identified some issues and informative findings.
Runtime Verification becomes Algorand Foundation’s security partner
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Runtime Verification Raises $5.3 Million to Advance Blockchain Security
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
MultiversX (formerly Elrond) gets new secure dev tooling and a formal semantics
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K-Michelson: a Case Study on Formal, Executable Language Specification (Part 2)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K-Michelson: a Case Study on Formal, Executable Language Specification (Part 1)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Runtime Verification completes another successful engagement with PlatON Networks
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Runtime Verification and Algorand announce a new engagement to build formal tools for Algorand’s smart contract ecosystem
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formal Verification Framework for Michelson
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formally Verifying Finality in Gasper: The Core of the Beacon Chain
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
KWasm and KEwasm: executable semantics and formal verification tools for Ethereum 2.0
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formal Verification 101 for Blockchain Systems and Smart Contracts: Formalizing Requirements
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Runtime Verification enters a protocol verification agreement with PlatON
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formal Verification 101 for Blockchain Systems and Smart Contracts
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K vs. Coq as Language Verification Frameworks (Part 3 of 3)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K vs. Coq as Language Verification Frameworks (Part 1 of 3)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K vs. Coq as Language Verification Frameworks (Part 2 of 3)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
A Formal Model in K of the Beacon Chain: Ethereum 2.0’s Primary Proof-of-Stake Blockchain
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Runtime Verification joins the Enterprise Ethereum Alliance
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
The RV Bounded Model Checker - A lightweight semantics-based tool
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
How Formal Verification Could Help to Prevent Gridlock Bug
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
A Subtle Rust Bug
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formally Verifying Algorand: Reinforcing a Chain of Steel (Modeling and Safety)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formal Verification of Ethereum 2.0 Deposit Contract (Part I)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Code smell: Boolean blindness
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Runtime Verification Completes Initial Formal Verification of Ethereum Casper Protocol
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Runtime Verification goes multinational by opening Bucharest based subsidiary
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
ERC777-K: Formal Executable Specification of ERC777
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formal Verification of ERC20 Contracts
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
How Formal Verification of Smart Contracts Works
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K Framework - An Overview
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
IELE: A New Virtual Machine for the Blockchain
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
RV Inc. & FSL @ UIUC Release First Formal Viper Tools
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
ERC20-K: Formal Executable Specification of ERC20
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
New Technologies for the Blockchain: IELE (virtual machine) and K (universal language framework)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
RV Inc. & FSL @ UIUC to Formalize Ethereum's Viper
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
RV-Match now supports inline assembly
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Let's Make the Ethereum Virtual Machine Better
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K Developer Interviewed in Illinois Paper
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
ASE 2001 paper that helped shape the Runtime Verification field got the Most Influential Paper Award
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
RV Employee Analyzes the DAO Attack
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
RV Inc. to Give Tutorial at Runtime Verification ’16 Conference
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
RV Could Make Cars Safer - Article in UIUC's Click Magazine
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
