Founded & Funded Can We Trust AI? The Future of Verified Reasoning in High-Stakes Systems
25 snips
Jan 22, 2026 
In this insightful discussion, Carina Hong, Founder and CEO of Axiom, introduces her work on AI that utilizes verified proofs for high-stakes reasoning. Byron Cook, VP at AWS, shares how formal verification secures vast cloud infrastructures. They explore the limitations of current AI models in truth verification, the significance of mathematical proofs in ensuring correctness, and the transformative potential of verified AI in finance, healthcare, and more. Together, they envision a future where AI can reliably assist in critical decision-making.
AI Snips
Chapters
Transcript
Episode notes
ML Lowers The Barrier To Formal Methods
- Usability improvements and ML integration are democratizing formal methods like Lean and Isabelle.
- Models trained with proof data can interact with provers, making verification approachable to more engineers.
Define Properties Then Prove Them
- Identify precise properties you want (e.g., encryption at rest, no memory corruption) before proving programs.
- Use mathematical induction and formal techniques to demonstrate those properties hold for your system.
Proofs As Executable Checks
- Turning math proofs into executable programs (Curry-Howard) gives automated pass/fail checks for correctness.
- A verifier's checkmark provides a deterministic feedback loop to train and improve reasoning models.