Runtime Verification had just reported bugs in the Linux kernel, the core of the Linux operating system, when Nathan Labenz, host of The Cognitive Revolution, put the obvious question to the company's leaders. Why hadn't this been caught before? What let these issues rise to the top when so many human reviewers had presumably "blown right past" them?
The company has spent about 15 years building tools that mathematically prove software does what it is supposed to do, Labenz said when introducing the segment on an episode published October 17, 2026. Everett Hildenbrandt, the CEO, and Grigore Rosu, the founder and a professor at the University of Illinois, joined Labenz and his co-host Prakash Narayanan. In their account, the result came from a slow, methodical pipeline in which a language model did one job inside a set of deterministic checks.
Starting with a guess about where bugs hide
Hildenbrandt answered Labenz's question by describing a hypothesis about where to look, reasoned out "in the same way you would think about, you know, making a formal specification." The team asked where the kernel receives untrusted input, and which parts probably get less scrutiny than others. That led them first to device drivers, the code that lets the operating system talk to attached hardware.
The method was built to raise confidence one step at a time. The team wrote a specification, a precise statement of what the code is supposed to do, and inspected the code against it. Then they had a language model port the existing C code into Rust, a newer language designed to rule out many memory errors. Next came differential fuzzing: feeding large numbers of random or malformed inputs to both the original C and the Rust port and comparing what each does. Because the port is meant to behave identically, any divergence points to a possible bug in the original C. Hildenbrandt said they found a bug at that stage. When they went on to verify the correctness of the Rust code, they found another.
They did not just point an LLM at the kernel and tell it to find bugs, he said, which "also works, by the way." But early LLM bug hunting turned toward designing harnesses and approaches, which he said "exactly mimics" the methodical process that human software quality assurance has followed for decades.
Two-week time boxes and one Claude Code instance
Some of the targeted kernel code was left unproven, and Narayanan asked why. The answer was that the code wasn't unverifiable: the experiment was time boxed, and when the box ended the team moved on to the next target. They tried a different target about every two weeks, refining the approach with the aim of turning it from an expert-level tool into something anyone can run on their own code base.
Narayanan pressed on what the time box meant in practice: two weeks with 10,000 agents, or two weeks with five? The reply was that agent use was light. It was a single instance of Claude Code, Anthropic's coding agent, on a premium plan, with a little more money added when the team hit session limits. The real constraint was human time.
The company also described a working rule: make things deterministic whenever possible. The answer suggested that people doing security analysis may be held back by assuming everything has to be driven by an LLM. If a model discovers a technique that works well, turn it into a tool and run the tool every time.
What the published write-ups show
Runtime Verification has described projects of this kind on its blog. These posts show what the pipeline looks like in practice; they are context, not confirmation of the specific cases discussed on the show.
An August 20, 2026 post follows one parser in the Linux driver for USB video devices (UVC) through extraction, a rewrite in safe Rust, differential fuzzing and verification in Lean, a program that checks mathematical proofs mechanically. After the team fixed a mismatch in its own port, fuzzing recorded zero divergences over 54,019 executions, reaching 93% edge coverage, a measure of how many of the code's branches the tests exercised. Another apparent divergence disappeared once the extracted C was compiled with the kernel's own compiler settings. A defect still turned up when the team inspected both versions side by side: incorrect frame-size arithmetic that could sometimes yield zero. After tracing how the value was used, the authors classified it as a correctness defect, not a live memory-safety hole. Another reporter had already identified the issue, and Runtime Verification joined the upstream patch work. The proofs were partial: the full theorem that the code never panics on well-formed input (the post treats a panic on malformed input as intended safe behavior) still depended on four unproven lemmas, and loop results covered five of eleven loops.
An October 2, 2026 report covers user namespaces, the kernel feature that maps user IDs inside a container to IDs on the host. Writing the specification exposed an unchecked conversion from a 64-bit number into a 32-bit field: asking for container ID 4294967296 installed ID 0 instead. Later permission checks still applied, so the authors called it an incorrect mapping rather than a security bypass, and a validation patch with a test was under review. A Rust reimplementation, mechanically converted into Lean, supported 89 proved theorems, with seven lemmas still open. The model covered tables already in memory, not the kernel's handling of many processes acting at once.
What a proof does and doesn't establish
The conversation turned to whether full Rust and Lean models of Linux could be formally verified within 24 months, a timeline the question linked to what some people on the AI safety side expect. The answer was confident that it would happen. It pointed to the company's tools for code translation and validation, and to deterministic tools that already turn Rust into Lean, which need more work and to which the company is contributing.
That answer drew a line between two kinds of guarantee. The translation tool can formally verify that Rust produced from C is behaviorally equivalent to the original, a drop-in replacement "bug for bug." That is different from verifying that the code is correct. An LLM can do the translation if you want, but the check is deterministic: either the Rust behaves the same as the C, or the tool turns up differences that can be sent back to the C developers.
The company makes a related point in a September 30, 2026 post, The proof is in the spec. Differential testing catches translation discrepancies empirically, but a checked theorem still depends on the model and specification faithfully representing the intended program. The workflow it describes starts with an English specification reviewed by maintainers, tests formal statements for vacuity (for example, assumptions that can never hold), and identifies the specification, assumptions and excluded components in every delivered result.
Winning over the maintainers
Hildenbrandt said the first approach to Linux kernel maintainers went badly. The team told them formal verification "has legs" and would help find bugs and make the software more secure. "They basically told us to go kick rocks," he said. He didn't blame them: they are busy, and people only adopt methods that bring them value. "You can't just go force people to do formal verification," he said, "like we can force agents to do it."
So the team changed tactics. It would do the automatic formalization, fuzzing and translation on its own end and ask nothing of the maintainers. What came out was "bugs and patches, bugs and patches," Hildenbrandt said, which is what maintainers value. After the team submitted a few, he said, it is being invited to explain how it did the work.
His longer-term goal is a Rust version of the entire Linux kernel and a separate Lean model of it. He said he doesn't want to burden maintainers with either until they see it as clearly valuable: "we're not going to force that down their throat."
A recipe for vibe coders
When the hosts asked what someone vibe coding an app, building it by describing what they want to an AI, should actually do, Rosu offered a simple recipe. Once the code is generated, tell the agent to write down the specification and prove the code correct. That will surface new errors, he said, because most errors are found while writing a specification, when you step back and ask what the code is trying to do. He expects an agent to go through the same process: "It's like a review plus plus."
The user-namespace project shows the specification step cutting both ways. According to the report, Claude Code helped build most of the 89 theorems, with Lean checking the proofs, but specification decisions were harder. Four confident claims about how the kernel behaves turned out to be wrong, and running the kernel or checking the arithmetic exposed the mistakes.
Hildenbrandt expects this to become normal practice. He said he firmly believes "writing code is a dead art in two years tops," replaced by writing specification and intent. Within five years at most, he said, delivering a package will mean answering more than whether it reached the registry and defined its API: "Did I provide the formal specs? Did I provide the lean proofs?" He said the era of the "cowboy coder" and "artisanal software" will end, and that software without a specification and formal verification attached won't fit in the package repository "because it just will be too risky." He also predicted that specifications and proofs will become part of how companies vet their software supply chains.