Formal methods are a branch of mathematics and computer science focused on proving the correctness of systems,

and they have long promised a more rigorous foundation for software.

However, their complexity has kept them confined to a small community of specialists.

That is now changing as agenic AI systems take on increasingly autonomous roles. The question of how to define,

enforce, and verify what those agents are allowed to do has become urgent, and automated reasoning

is emerging as a critical part of the answer. Byron Cook is a VP and distinguished scientist

at AWS, a professor at University College London,

and a program manager at DARPA. He founded the automated reasoning group at AWS over a decade ago,

where his team built the foundations behind products like IM Access Analyzer, VPC Reachability

Analyzer, and Bedrock Guardrails.

In this episode, Byron joined Sean Falconer to discuss how automated reasoning works

and why it scales so well with AI.

The rise of neuro-symbolic approaches that combine formal logic with large language models,

what it means to formally specify agent behavior using temporal logic, and why the convergence of agentic AI and formal methods may

represent one of the most significant shifts in how software is built and verified.

This episode is hosted by Sean Falconer. Check the show notes for more information on Sean's work and where to find him.

Byron, welcome to the show.

Thank you very much.

Thanks for having me.

Yeah, absolutely.

Looking forward to this.

So we're going to probably cover a lot of ground today.

...