Formal Methods as Agent Guardrails
Podcast: Play in new window | Download
Subscribe: RSS
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.
Please click here to see the transcript of this episode.
Sponsorship inquiries: sponsor@softwareengineeringdaily.com
Sponsors
You know Fidelity as a financial services leader. But did you know that inside Fidelity is a community of technologists working together to shape the future of finance and tech?
Fidelity is always investing in tomorrow: from emerging tech to cutting-edge tools that will transform what comes next. Their technologists are encouraged to keep learning so they can expand their skillsets, explore new ground, and stay ahead of this rapidly-evolving industry.
And right now Fidelity is hiring technologists to join their team.
Fidelity technologists get the best of both worlds: startup energy that’s grounded in the stability of a financial institution. That means support, resources, and amazing benefits.
Bring your skills to a culture where you’re empowered to dream big and build the tech that drives an organization and makes a real impact on people’s lives.
Find out more at Tech.FidelityCareers.com. That’s Tech.FidelityCareers.com.
Fidelity is an equal opportunity employer.
In mobile application security, ‘good enough’ is a risk.
Guardsquare uses advanced, multi-layered code hardening techniques and automated runtime application self-protection and mobile application security testing, combined with real-time threat monitoring, to deliver the highest level of mobile app security.
Discover how Guardsquare brings all these together to provide mobile app security for your Android and iOS apps without compromise at www dot Guardsquare dot com.
Every AI team eventually hits the same wall. The models are solid, the infra is solid, but the data coming in is hours old because the pipeline is batch when it should be streaming and nobody’s had time to fix it. That’s not a modeling problem. That’s a pipeline problem.
Estuary gives you CDC, batch, and streaming in one platform. 200 plus connectors, live in hours, not weeks. Your AI is only as good as your pipeline. estuary.dev
