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

What It Covers

Kathleen Fisher of RAND and Byron Cook of AWS explain how formal methods—mathematical techniques that prove software correctness—can dramatically improve cybersecurity before AI-powered attacks become ubiquitous, including AWS's automated reasoning systems.

Key Questions Answered

• •Formal Methods Spectrum: Type checkers in Java represent simple formal methods proving basic properties like integer operations, while interactive theorem provers like CompCert verify full functional correctness of C compilers down to assembly code, requiring PhD-level expertise but providing complete semantic guarantees with explicit assumptions about hardware.
• •AWS Security Implementation: Amazon applies formal verification across critical infrastructure including TLS handshake protocols in s2n, policy interpreters handling over one billion calls per second, and the new isolation engine hypervisor for Graviton five processors, using tools like SAT solvers and Isabelle theorem prover to prove cryptographic correctness and separation properties.
• •AI-Assisted Proof Generation: Generative AI models now find inductive invariants and ranking functions needed for proving program correctness with loops and termination, reducing previously intractable problems to combinatorial reasoning that automated tools handle efficiently, enabling one-to-one ratios of engineers to formal methods experts instead of requiring dedicated PhD specialists.
• •Automated Reasoning Checks: AWS translates natural language policies like HR handbooks into formal logic using multiple LLM translations verified for equivalence by theorem provers, achieving 99% verification accuracy by checking AI agent outputs against formalized rules, iteratively refining specifications through corner case analysis with domain experts providing ground truth validation.
• •Security Rewrite Timeline: Current software vulnerabilities remain equivalent to unlocked doors and open windows, but combining formal methods with AI code generation enables superhuman secure code production within two model generations, with memory safety, input validation, and parser-generated protocols eliminating entire vulnerability classes if society prioritizes deployment over feature velocity.