AIAM

EPISODE 2026-10-12

AI-Generated Code, Formal Verification, and Agent Security

Everett Hildenbrandt and Grigore Rosu discuss AI-generated code, Linux verification, software specifications, and the human role in agent security.

▶ Full show on YouTube

Everett Hildenbrandt and Grigore Rosu explain what verification can prove—and why human intent still matters.

The rundown

  1. 2:36Opening4 min
    Opening
  2. 6:57Interview33 min
    Everett HildenbrandtEverett HildenbrandtGrigore RosuAI coding and formal verification: who checks the requirements when agents can generate both software and proofs? Everett Hildenbrandt, CEO of Runtime Verification, whose team is verifying selected Linux components, and Grigore Rosu, Founder of Runtime Verification and creator of the K Framework, discuss why Hildenbrandt expects manual coding to disappear within two years. They describe AI driving theorem provers and a Linux assurance workflow that combines specifications, AI-generated Rust rewrites, fuzzing and proofs—but still depends on human review and useful fixes that maintainers can accept. Their argument lands on the developer's continuing responsibility: approve what the software should do, specify its interfaces and check that the evidence addresses those requirements. How reconstructing Linux's intended behavior exposed defects—and why a verified Rust rewrite can preserve the original C bugs. Why one Claude instance supported two-week verification trials, while more AI-generated patches could overwhelm human maintainers. How proved monitors and dependable components can support agent creativity without proving the entire agent correct.

    Watch

    Open segment on YouTube ↗

    Clips

    • AI security: Why Linux patch floods can backfire

      0:00 / 0:00

    • Claude AI drafts a CEO's campaign without an agent swarm

      0:00 / 0:00

    • AI Linux rewrites: Two years to Rust and Lean models

      0:00 / 0:00

    • AI coding: Will manual programming end within two years?

      0:00 / 0:00

    • Linux proof experiments: One Claude Code instance

      0:00 / 0:00
  3. 40:03Segment7 min
    Post Guest Discussion
  4. 47:05Segment11 min
    YPO Conference Review
  5. 58:30Closing3 min
    Closing

In this episode

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.

  • AI coding and formal verification: who checks the requirements when agents can generate both software and proofs? Everett Hildenbrandt, CEO of Runtime Verification, whose team is verifying selected Linux components, and Grigore Rosu, Founder of Runtime Verification and creator of the K Framework, discuss why Hildenbrandt expects manual coding to disappear within two years. They describe AI driving theorem provers and a Linux assurance workflow that combines specifications, AI-generated Rust rewrites, fuzzing and proofs—but still depends on human review and useful fixes that maintainers can accept. Their argument lands on the developer's continuing responsibility: approve what the software should do, specify its interfaces and check that the evidence addresses those requirements. How reconstructing Linux's intended behavior exposed defects—and why a verified Rust rewrite can preserve the original C bugs. Why one Claude instance supported two-week verification trials, while more AI-generated patches could overwhelm human maintainers. How proved monitors and dependable components can support agent creativity without proving the entire agent correct.