Show Notes
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: [email protected]
The post Formal Methods as Agent Guardrails appeared first on Software Engineering Daily.
More from Software Engineering Daily
Codebases in enterprise organizations often span hundreds of thousands, or even millions, of lines of code. In many cases, changes must follow established patterns precisely, or risk introducing costly security or operational issues. A common challenge with AI coding tools is that they struggle at this scale: LLM context windows cover only a fraction of a large codebase, and output quality degrades the longer an agent runs.
In recent years, the main impact of AI has been on the digital world, and most notably software engineering. However, its longer-term effect on the physical world may prove even more profound, reshaping how cars drive themselves, how factories run, and how robots move through homes and warehouses.
Software testing is widely understood as essential to building reliable systems, and it’s one of the hardest things to get right. A fundamental issue is that tests are good at confirming the behavior a team expects, but the most damaging failures tend to hide in the edge cases no one thought to check during development. Those blind spots are only growing as AI produces more code that no human has closely reviewed.
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.
The popular story of Steve Jobs is that he co-founded Apple, was pushed out, wandered through a failed venture called NeXT, then returned to save the company and usher in the iPod and iPhone. That version is memorable, widely repeated, and, in an important sense, wrong. His years at NeXT are usually treated as a footnote, when they were among the most consequential of his life and career.