Technical writing from the Runtime Verification team on safety-critical software, formal methods, security research, fuzzing, audits, and the systems that must keep working when failure is not acceptable.
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.
AI-written formal proofs find real bugs. But a checked proof only verifies its own model and spec — here's what that means, and how to get it right.
We used AI-assisted differential fuzzing to find bugs in WebAssembly runtimes, and it found a real bug in WAMR, while also confidently flagging behavior that turned out to be valid. The experiment shows where AI is already extremely useful in security testing: generating evidence and accelerating investigation, while leaving the final judgment to human expertise.
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.
Runtime Verification and Assurea Partner to Strengthen Software Safety for Medical Devices, SaMD and Artificial Organs
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.
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.
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.
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 Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
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.
