"The Cognitive Revolution" | AI Builders, Researchers, and Live Player Analysis The Great Security Update: AI ∧ Formal Methods with Kathleen Fisher of RAND & Byron Cook of AWS
88 snips
Dec 24, 2025 
Kathleen Fisher, director at RAND and incoming CEO of ARIA, and Byron Cook, VP at AWS, share their pioneering insights into automated reasoning for cybersecurity. They explore how formal methods can enhance software security against AI-driven cyber threats. The duo discusses the significance of memory safety and policy verification while delving into AWS's innovative approaches to proving key components. They also envision a future where generative AI aids in creating more secure code, sparking a major rewrite of existing systems for better resilience against vulnerabilities.
AI Snips
Chapters
Transcript
Episode notes
Why Formal Methods Raise Assurance
- Formal methods provide machine-checkable proofs that raise software assurance far above ad-hoc testing.
- They trade absolute certainty for dramatically higher confidence by making assumptions explicit.
Pick The Right Verification Depth
- Choose the right level of formal method for the risk: use simple checks (types) for common errors and deep proofs for critical components.
- Balance effort and payoff when deciding what to verify for each system.
Composing Proofs Scales Assurance
- Proving parts of a cloud system leads to proofs that begin to touch and compose across components.
- Small proved components can grow into stronger system-level assurance over time.