Formal Methods as Agent Guardrails

Formal Methods as Agent Guardrails

Author: Software Engineering Daily May 19, 2026 Duration: 48:32

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 agentic 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 IAM Access Analyzer, VPC Reachability Analyzer, and Bedrock Guardrails.

In this episode, Byron joins Sean Falconer to discuss how automated reasoning works and why it scales so well with AI, the rise of neurosymbolic 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.

Sean’s been an academic, startup founder, and Googler. He has published works covering a wide range of topics from AI to quantum computing. Currently, Sean is an AI Entrepreneur in Residence at Confluent where he works on AI strategy and thought leadership. You can connect with Sean on LinkedIn.

Please click here to see the transcript of this episode.

Sponsorship inquiries: sponsor@softwareengineeringdaily.com

The post Formal Methods as Agent Guardrails appeared first on Software Engineering Daily.


Dive deep into the conversations that shape how we build and understand complex systems with Data Archives-Software Engineering Daily. This podcast pulls from a rich library of technical discussions, each one a focused exploration into the specific tools, architectures, and challenges that define modern software engineering. Rather than surface-level news, these episodes offer sustained, thoughtful dialogues with the engineers and thinkers who are working on the front lines of data infrastructure, distributed systems, and emerging technologies. You'll hear detailed breakdowns of real-world problems and the nuanced solutions teams are implementing, providing a practical sense of how theoretical concepts translate into production code and resilient platforms. The archive serves as an enduring resource, whether you're looking to grasp the fundamentals of a new database or understand the intricate trade-offs in a system design. Tune in for a consistently substantive listen that treats software engineering with the depth and seriousness it deserves, all through the unfiltered lens of expert conversation.
Author: Language: en-us Episodes: 50

Software Engineering Daily
Podcast Episodes
A Rust Framework to Simplify Distributed Systems [not-audio_url] [/not-audio_url]

Duration: 50:31
A Rust Framework to Simplify Distributed Systems Building software that runs across many machines is notoriously difficult. Developers have to grapple with problems such as race conditions, partial failures, and message…
Moving Beyond RAG with Precomputed Context [not-audio_url] [/not-audio_url]

Duration: 55:48
Retrieval has become one of the central problems in building useful AI systems. The standard approach to grounding a model in one’s own data has been retrieval augmented generation, or RAG, where an agent searches a vect…
The Death of Online Anonymity [not-audio_url] [/not-audio_url]

Duration: 52:42
Age verification is reshaping how people access the internet. An ever-growing patchwork of laws can now require government IDs, facial age estimation, or behavioral inference before you can enter digital spaces. Discord,…
TypeScript 7 and What Comes Next [not-audio_url] [/not-audio_url]

Duration: 57:15
TypeScript is a programming language that builds on JavaScript by adding a system of types. Those types let developers describe the shape of their data and catch mistakes before code ever runs, while also powering the au…
The Gap Between AI Spending and AI Value [not-audio_url] [/not-audio_url]

Duration: 54:42
It is widely reported that a gap has emerged between enterprise spending on AI and the durable value captured from that spend. Individual employees have enthusiastically adopted coding assistants and chatbots, yet those…
AI and the New Global Security Landscape [not-audio_url] [/not-audio_url]

Duration: 1:12:32
The conversation about AI often focuses on software, automation, and the race between attackers and defenders in code. However, some of the most consequential risks lie further afield, in domains where a mistake is measu…
How LLMs Are Reshaping Recommendation Systems [not-audio_url] [/not-audio_url]

Duration: 47:51
News feeds and recommendation systems have long relied on deep learning architectures that score each candidate item independently. As LLMs have matured, they have opened up a fundamentally different approach, where a sy…
Rebuilding the Cloud for AI Agent Code [not-audio_url] [/not-audio_url]

Duration: 49:57
For two decades, the cloud has been shaped by human developers writing code and managing its deployment. Now a growing share of production code is generated by LLMs with little human review. Because that code is not full…
SED News: The Kimi Moment, Runaway AI, and Tokenmaxxing [not-audio_url] [/not-audio_url]

Duration: 48:28
SED News is a monthly podcast from Software Engineering Daily where hosts Gregor Vand and Sean Falconer break down the biggest stories shaping software engineering, Silicon Valley, and the broader tech industry. In this…