The Great Security Update: AI ∧ Formal Methods with Kathleen Fisher of RAND & Byron Cook of AWS

Hello, and welcome back to the Cognitive Revolution. Two quick notes before we jump in today. First, again, applications for the MATS 2026 summer program are now open. At NeurIPS this year, MATS fellows presented many papers at at mechanistic interpretability and alignment workshops, and six MATS Fellows had spotlight papers. So if you're interested in a career in AI safety research, you should definitely consider applying. I'm also excited to say that I've booked MATS executive director, Ryan Kidd, for a full episode early in the new year. So listen to that and be prepared to submit your application by the January 18 deadline. Second, we're planning to record another AMA episode probably in the 2026. Visit our website, cognitiverevolution.ai, and click the link at the top to submit your questions, or feel free to DM me on your favorite social network. With that, today, we're diving into the world of automated reasoning and formal verification of software. My guests, Kathleen Fisher and Byron Cook, are legends in this underappreciated but increasingly important field. Kathleen famously led the High Assurance Cyber Military Systems or HACMS project at DARPA, is currently the director of the cybersecurity initiative at RAND. And starting in February, will take over as CEO of The UK's Advanced Research and Invention Agency, ARIA, which is often described as The UK's DARPA, though its mission goes beyond military technology with the goal of unlocking scientific and technological breakthroughs that benefit everyone. Byron, meanwhile, is vice president and distinguished scientist at Amazon, where he's made a major contribution to cloud security by leading the application of formal methods to distributed systems at AWS, which despite being arguably the world's biggest target for cyber attackers, has maintained an amazingly strong security record. In all honesty, I don't think I've ever felt more outclassed by my guest than I did in this conversation. My own math career topped out at differential equations and complex analysis in college, and I've never been strong when it comes to mathematical proofs or formal logic. Nevertheless, I'm hearing more and more in AI circles, not just about the need to harden critical infrastructure against cyber attacks before AI powered hacking becomes ubiquitous, but specifically about the unique power of formal methods to deliver true information security guarantees. And so I was really eager to learn as much as I could and honored that these masters were willing to answer my remedial questions. We cover a lot of ground in this conversation, from the nature of the cybersecurity threats that AI poses to the relationship between software specifications and the proofs generated by formal methods to the critical role of assumptions and how it is that we can be confident that many low level logical statements do in fact add up to system level guarantees. We also discuss how these methods can be used to create a reward signal for coding models and why, despite what we've seen from AI coding assistance to date, we …