Category: Verification

A policy bypass in io_uring's sandbox filter, found by writing down what the filter should see. The bug, the reproducer, and a fix in mainline in a day.

Optimism's Supernode decides which cross-chain messages are valid and advances the cross-safe frontier: get it wrong in one direction and a chain builds on invalid state; wrong in the other, and the whole cluster stalls. This post covers a hand-written Dafny model of its core logic we built during a 10-week audit extension, and how we used it as the basis for AI-assisted fuzzing and comparison against the Go implementation.

We verified a core piece of the Linux kernel's container isolation code in Lean 4, and writing the spec turned up a parsing bug we've sent a fix for upstream. We also learned where AI speeds up proofs and where it gets the specification wrong.

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).