Category: Verification

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.

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.

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.

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.

In this blog post, we'd like to share how we build formal verification and fuzzing tools, highlight some of the projects we've developed—such as Kontrol, Kasmer, and Komet — and delve into what it takes to create a tool for formal semantics. Our goal is to provide insights for teams interested in using and developing similar tools for their smart contract languages or ecosystems.

This blog post continues our journey into formal verification of loops in Solidity and EVM smart contracts. It introduces loop invariants, a challenging but essential technique for reasoning about unbounded loops. We explore natural induction, apply pen-and-paper methods, and then leverage Kontrol to formally prove the equivalence of two Solidity functions, diving deep into EVM bytecode and formal verification tools.

Explore the challenges of formal verification in Solidity and EVM smart contracts. Learn about the path explosion problem, bounded loop unrolling, and how tools like Certora Prover, Halmos, hevm, and Kontrol approach verifying loops in smart contracts.

Stay updated on KMIR's development progress as Runtime Verification defines the semantics of Rust's Middle Intermediate Representation (MIR) in the K Framework. Learn about Stable MIR serialization, the smir_pretty driver, and the future of KMIR's symbolic execution capabilities.

Runtime Verification completed a design review of Lido's dual governance mechanism. This mechanism is the first of its kind, representing a monumental upgrade to the Lido governance model. This collaboration aimed to ensure that the new system, scheduled for testnet release in Q3 2024 and mainnet in Q4 2024, functions as intended and maintains the integrity and security of Lido’s $33 billion in total value locked (as of this writing).

This is the 3rd post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This post will explain a crucial feature we developed in Kontrol to verify the pausability mechanism in a realistic scenario. This new Kontrol feature allows loading a transcript of the effects of executing a function directly into proofs, which effectively means having a part of a Kontrol proof computed by Foundry!

This is the second post of a three-part series about our recent Optimism engagement, in which we verified their pausability mechanism for L1 contracts. This installment explains how Kontrol can be used to tackle the complexities caused by dynamically-sized constructs and the challenges associated with the loops that result from them.

Learn how Runtime Verification's contribution to the Stable MIR project enhances Rust development by implementing Serde serialization. Discover how this key addition improves accessibility, portability, and future project development using Rust’s Middle Intermediate Representation (MIR).