Category: Verification

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.

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.

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.

How We Build Formal Verification and Fuzzing Tools: Bridging the Gap Between Developers and Advanced Security Tooling with the K Framework

By Gregory MakodzebaDecember 10th, 2024

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.

Formally Verifying Loops: Part 2

By Raoul SchaffranekOctober 7th, 2024

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.

Formally Verifying Loops: Part 1

By Raoul SchaffranekSeptember 26th, 2024

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.

KMIR: Progress Update

By Daniel CummingSeptember 13th, 2024

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.

With $33B TVL on the Line, Lido Turns to Runtime Verification for a Design Review

By Runtime VerificationSeptember 4th, 2024

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

External Computation with Kontrol: Leveraging Foundry Execution for Formal Verification

By Juan ConejeroAugust 28th, 2024

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!

Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs

By Runtime VerificationAugust 19th, 2024

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.

Enhancing Stable MIR with Serde Serialisation

By Daniel CummingJuly 27th, 2024

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

Formal Verification Lore Intuitive Intro to Why We Can Prove Programs Correct

By Juan ConejeroApril 2nd, 2024

This article aims to provide context to formal verification, its different approaches, and why it can provide ultimate assurance of code correctness. Throughout the article, we provide insights into the field of formal verification and some of its components rather than explain how to use a specific tool. These insights should make it clearer to the newcomer to the field why we can claim mathematical rigorousness when we perform formal verification.

Introducing KMIR: concrete and symbolic execution of Rust MIR

By Daniel CummingNovember 20th, 2023

Runtime Verification is excited to announce the open public alpha of KMIR. KMIR defines the formal operational semantics of the Middle Intermediate Representation (MIR) of Rust in K, giving developers access to the K framework tool suite for MIR programs.