As AI systems take on more of the work of writing software, what does it mean to know that the result is safe? Everett Hildenbrandt, CEO of Runtime Verification, and Grigore Rosu, the company’s founder and creator of the K Framework, discuss AI-driven theorem proving and their work verifying selected Linux components. Their workflow combines specifications, AI-generated Rust rewrites, fuzzing, and proofs—but verification still depends on people defining what the software should do and checking that the evidence answers the right questions.
Prakash Narayanan and Nathan Labenz also examine the limits of verified rewrites, the burden AI-generated patches can place on maintainers, and the distinction between formal verification and AI alignment. The conversation ranges from agent security and shared infrastructure risks to autonomous vehicles, AI-generated conference keynotes, and practical safeguards for agents.
Show Notes
Runtime Verification CEO Everett Hildenbrandt and founder Grigore Rosu discuss AI-generated code, formal verification, Linux kernel rewrites, and the human role in setting specifications and reviewing evidence. Prakash Narayanan and Nathan Labenz also explore agent security, AI alignment, infrastructure risk, autonomous transport, and how organizations should work with AI agents.
Chapters
(0:00) When AI writes and verifies code
(2:36) Claude locked Nathan out of his own agent console
(3:56) What airlines know about falling back to paper
(5:40) Should we let China hit AI risks first?
(6:57) Meet Everett and Grigore from Runtime Verification
(8:05) Vague specs and unchecked libraries are the status quo
(11:40) AI already generates specs and drives provers
(14:37) Everett gives hand-written code two years
(16:24) Why human review missed the Linux kernel bug
(19:50) Prove the monitor, not the entire agent
(21:30) Linux maintainers wanted fixes, not another workflow
(22:44) Verified building blocks free agents to be creative
(25:53) One Claude instance, time-boxed by human hours
(27:28) More AI patches can burden Linux maintainers
(30:29) A Rust rewrite can preserve Linux bugs
(31:39) Claude assists Everett’s campaign without an agent swarm
(33:09) The specification still starts with human intent
(37:54) Write down intent before choosing a language
(39:27) Specify the API boundary before accepting software
(40:03) Formal verification does not guarantee AI alignment
(42:14) Industry-wide AI failures could trigger collective bailouts
(44:01) A shared AI layer could disable critical infrastructure
(45:20) Why do passenger planes still need human pilots?
(46:18) Should autonomous cars keep their steering wheels?
(47:05) AI builds keynotes from short DM exchanges
(49:56) Rent the intelligence, own the context
(52:17) AI spotted cancer before it could do taxes
(53:12) Give your agents a panic button
(54:06) The five x estimate might be too low
(55:20) Agents emailing agents, with three layers of protection
(58:30) AI swarm sets 300 new records in five days
(1:00:01) Why Nathan gives his AI tools away for free
Guests
Everett Hildenbrandt — CEO, Runtime Verification (𝕏)
Grigore Rosu — Founder, Runtime Verification (𝕏)
