Blog
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.
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.
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.
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
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.
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.
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!).
