Formal Methods as Agent Guardrails

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 https://x.com/byroncook is a VP and Distinguished Scientist at AWS https://aws.amazon.com/, 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. https://i0.wp.com/softwareengineeringdaily.com/wp-content/uploads/2023/10/Rectangle-3-2.pngSean’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. http://softwareengineeringdaily.com/wp-content/uploads/2026/04/EQ-edits-SED1918-Automated-Reasoning-1.txt Sponsorship inquiries: [email protected] https://cms.megaphone.fm/organizations/619b680e-d813-11ea-9750-e7ecac406436/podcasts/e60108fe-e328-11ea-b2b6-1348249f900a/episodes/3913370a-bc44-11ed-ace6-8b1f96d82bba/[email protected] The post Formal Methods as Agent Guardrails https://softwareengineeringdaily.com/podcasts/formal-methods-as-agent-guardrails/ appeared first on Software Engineering Daily https://softwareengineeringdaily.com.

• 0:00Speaker 00

  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.

• 0:42Speaker 00

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

• 1:27Speaker 00

  Check the show notes for more information on Sean's work and where to find him.

• 1:43Speaker 01

  Byron, welcome to the show.

• 1:45Speaker 02

  Thank you very much. Thanks for having me.

• 1:46Speaker 01

  Yeah, absolutely. Looking forward to this. So, we're gonna probably cover a lot of ground today. You've had a pretty rich history, but one of the things I wanted to start off with was, so you're a VP and distinguished scientist at AWS. You've been there over 11 years. You're also a professor at UCL and a PM for DARPA. So my first question, I guess, was like, how is all that possible? There seems like a lot of jobs to balance. How do you manage wearing those three different hats simultaneously?

• 2:13Speaker 02

  Cognitively, they're kind of the same job, right? I think in each role, I'm trying to identify really big things that other people can't wrap their head around, that maybe they don't think are possible. I'm trying to move the seemingly impossible to the possible and then trying to de-risk that. So like either trying to establish basis for confidence or prototype stuff. And that often involves getting people in the orbit of the scientific world and the startup world and the university world to like, find the right people with the right tools to like prototype something and then simultaneously write some sort of report or some sort of PowerPoint document or something, something in the language of the institution to help them appreciate what's possible.

• 2:56Speaker 02

  To give your leaders a lever to pull on to prioritize these kinds of things. And so it's all kind of the same, like it's sort of like the difference between Spanish and Portuguese. You're using slightly different nouns and verbs, but largely they're in the Indo-European family of languages. And so you're kind of doing the same thing in these large organizations. They all kind of speak the same language. So, and then even if I'm at Amazon, I'm at any given time have three or four things going on. So I'm sort of context switching between those things anyways.

• 3:23Speaker 01

  Was that something that you were always interested in, trying to tackle these types of problems that seem impossible?

• 3:29Speaker 02

  I saw my father work between institutions and basically see the community as his stakeholders or his customers or the people he was working with and sort of cross organizational boundaries. And then I, like in my life, I'm working on cars or doing music or these kinds of things. People sort of are floating in and out of organizations and you're sort of just trying to solve problems together. So I've always kind of seen the organizational boundaries as relatively porous. And then I got really interested in logic and it's a very small crowd of people. So there's maybe 3,000 people in the world who specialize in this area. And so we're always at different institutions, different places, meeting up with each other. And then it's kind of like bands, like you tend to like with three or four people realize there's something really cool to go after. You go after it for two or three papers.

• 4:12Speaker 02

  And then kind of after that, then people often kind of drift off and do the next thing. And so to me, it's very fluid and the particular details of the organization don't really matter. I'm just. Usually be in the place that's sort of the best place for me to be in to help the community figure out household problems.

• 4:26Speaker 01

  Yeah, and one of these things is one of the kind of seemingly impossible things that you were able to kind of show was potentially possible was around essentially you built a tool that could automatically prove whether certain types of programs could terminate. And making a significant contribution essentially to the halting problem.

• 4:45Speaker 02

  Yeah.

• 4:45Speaker 01

  I guess like what made you believe that something like that was solvable, given that I'd say like conventional wisdom and even Alan Turing essentially said otherwise?

• 4:55Speaker 02

  Yeah, so there is a theorem that the problem is undecidable. That's a very meaningful result, right? That means that you cannot build a tool that can take any program in as an input and always itself terminating with an answer and always giving a right answer. You have to cut a corner somewhere. And so you can cut the corner by saying, well, relax the restriction that always has to give an answer. Well, we'll be okay with maybe the tool not giving the answer from time to time. And then we'll just they'll say, well, maybe we can get that. The occurrences of it not giving an answer down to some level where we're actually still getting value from the tool. And so that's sort of reframing the theoretical result from Godel and Turing is fundamental and absolutely staggering. But on the other hand,

• 5:39Speaker 02

  there's lots of things that are unsafe that we do all the time. Driving is unsafe. But we get in the car and if we get to our destination, then we know we got there safely. And so the insider bound that area is really interesting. I was actually working in the Windows kernel team. And I was carpooling with a person who's a developer in the Windows kernel team. And he kept when we're talking about things that should hold of the kernel, he kept using the word eventually. Like that if this happens, that eventually should happen. And I realized that was like, that is the termination question. It's like termination in the word eventually sort of have there's a theoretical result that sort of connects them saying they're essentially the same thing. And so I realized that was an important problem. And then I began thinking about what tools could we put together from existing pieces we already had to do something quite quickly for device drivers?

• 6:22Speaker 02

  And then that was successful. And then that turned into reasoning about biological systems and it turned into reasoning about. Non-blocking concurrency and so on.

• 6:29Speaker 01

  Yeah. And was the original focus on device drivers, was that partly motivated because at that time, like, device drivers was one of the biggest culprits of essential failures in operating systems?

• 6:40Speaker 02

  Yeah. So in the 1980s, if your computer crashed, you just, it was like, well, it's sad you lost your little word processing document or whatever you're working on. But as we went to data centers, the, the difference between crashing and not crashing was sort of the difference between the customer choosing your product or not. So it became important to root out those crashes. And it turned out that in the early 2000s, 85% of crashes in the operating systems were actually due to device drivers. So it was, it became an important problem to work on.

• 7:05Speaker 01

  Wow. Yeah. Yeah. Talk about, you saw that as a high ROI, I guess, to this day.

• 7:12Speaker 02

  And they were really neat because the device drivers were not actually that big. You know, they're like 80, 200,000 lines of code or 80,000 lines of code. You know, they'd have like 60 loops. Data structures they were operating over were actually relatively simple. They were cyclic doubly linked lists. So in many ways, it was actually a slightly, it was an easier problem than the, from a more general problem. So then we were able to do some really neat things that kind of were tuned to that domain, which sort of allowed us to bypass some of the, not theoretically, but we practically bypassed some of those challenges around undecided ability.

• 7:44Speaker 01

  Yeah. So in a lot of ways, you're bounding this unbounded problem, right, to a more specific class of the problem?

• 7:51Speaker 02

  Yeah. You can't solve the problem in generality. So you're going to have to identify niche areas where while it's still my timeout from time to time, it's not going to timeout enough to cause sufficient pain to the person using it for their niche domain. And the only hope is to get as close as you can to the person who's with the understanding of the niche problem to kind of understand the dynamics of that problem. So that, that happened again with reasoning about genetic regulatory pathways, where I was like, oh, I see. So usually they have this shape and usually they're of this size. Usually they're asking this kind of question. So actually, we could do something that 95% of the time is actually going to give them an answer and maybe 5% of the time it says, sorry, I can't answer the question.

• 8:30Speaker 01

  But. Okay. So you founded the automated reasoning group at AWS like over a decade ago. What was that original pitch to the Amazon leadership for them to be excited and want to believe in this?

• 8:42Speaker 02

  Let's see. So I I had kind of exhausted. I mean, I'd written all the research papers. You know, I was like, how much more can I do in this ivory tower research environment that I was in at the time? So I was sort of looking for a place to go where I could maybe have more breathtaking impact with the work I was doing. And so I actually sort of, I went and talked to a bunch of potential employers and kind of figured out which one I would want to work for. And I think that AWS was pretty happy to have me because they, it was pretty risk free, right? Like I was going to join, they were only hiring one person. I report directly this as though if I think if it didn't work out, then I would exit. I would imagine that would be the discussion that they were having, like, how risky is this hire?

• 9:25Speaker 02

  And then what Amazon, I think, does a really good job of traditionally is incrementally investing in things that are working. So they look for signs of direction of change on things that are going well. And they have a whole language around year over year change and so on. So they look for bets that are going well, and then they continue to feed the bets and like double down on bets. And so it's a whole calculus of what to double down on and how to prioritize things. So once I got in the system, then Amazon just naturally went through its mechanisms of prioritization and it just grew like a weed, really.

• 9:55Speaker 01

  Mm hmm. You know, given that like AWS runs critical infrastructure for millions of customers, like going back to some of your, your work with like the drivers and sort of proving whether they can run successfully or not, like, are there similar class of problems around? I am policies and network configs and things where if you mess those up, it can go really bad. Is someone operating this type of infrastructure? Is there a way to essentially apply some of your work to those areas?

• 10:22Speaker 02

  Yeah. So that's what we did. So when I first joined, I identified, you know, I went and chatted with a bunch of people and looked at a bunch of documentation and kind of identified the top 20 security concerns or issues or cliff calls and so on. And then prioritize them by what I thought the kinds of things that I had done in the past could help on. Identified four or five of them, hired a few of my friends, and then we kind of went after them. And so, yeah, you identified two of them so that one is reasoning about the semantics of AWS policies. Another one is the virtual networks, because if you get those wrong, then you're gonna have a really bad day. And then we also worked on like low level code, like virtualization and cryptography. And then we also worked on like the distributed systems protocols.

• 11:03Speaker 02

  So how do you, for example, maintain secrets across a distributed system such that they're highly available and durable and so on? So the thinking around protocols and distributed systems was another area. And then each one we went after with great gusto. And then the idea is that if any one of those projects were successful, then we'd be successful. And fortunately, but unfortunately, they were actually all successful. So then I spent two or three years really holding on to many high voltage wires as I was trying to get each of those projects kind of. They were all quite hungry to move to the next level. And I kind of found myself to be the bottleneck on the communication around how to grow those things and how to get them into the right place. So it took me a couple of years to get out of that.

• 11:45Speaker 01

  Yeah, how's that work? I'm assuming like your teams and yourself, you know, especially when you were essentially an IC functioning in this role until you hire some of your friends and so forth. But like you're sort of doing this as this like research project, I assume. And then maybe you're doing the proofs, maybe there's P O C involved. Like, how do you go from that essentially to this thing running in production and serving millions of people?

• 12:04Speaker 02

  So one piece of advice I got when I first started was the person was like, hey, you know, like in the previous employers, you've gone for these moonshots, right? You have these crazy big things, but what you want to do here is you want to find a moonshot ladder, right? You want to find every quarter, every six months, you want to deliver something that if people don't have any context on your bigger picture, why you're doing it, what's possible? In fact, you probably don't even want to tell them the bigger picture, deliver that. But then you know that each piece, each delivery sort of adds up to the bigger moonshot that you're going after. And so focus on it that way. And Amazon is a very sort of show me kind of place where they, people kind of believe it when they see it. So rather than talking about what you can do, deliver something maybe a lot smaller than you normally would. Build trust through that and then iterate, iterate, iterate.

• 12:49Speaker 02

  And so we, the projects that we were very successful on were those that we were able to break up the bigger moonshot into a much smaller set of steps. And for those that we weren't able to, they languished and it was only once we'd sort of. Built trust and built momentum on some of these others that we were able to come back to this bigger things and take them on again.

• 13:07Speaker 01

  That makes sense. Just even my experience, having worked at a variety of different startups, when you kind of start in a new role, a lot of times, it's like, how do you build to something big, but also how do you show value as soon as possible?

• 13:18Speaker 02

  Yeah.

• 13:19Speaker 01

  And it's much easier to do that with a smaller, more constrained project.

• 13:22Speaker 02

  Yeah.

• 13:23Speaker 01

  And then as you build trust, people kind of believe in maybe the bigger thing and the longer term deliverable.

• 13:28Speaker 02

  Yeah, yeah, exactly.

• 13:29Speaker 01

  Is there any challenges around from an engineering perspective where when you're thinking about like formal verification, and you're doing that sort of in the lab, that doesn't necessarily need to be as fast as it might need to be when you're actually delivering this type of stuff in production? Is there ever a challenge there where the formal verification perhaps in the lab environment is slow? And then how do you sort of engineer it to something that can run in production at scale?

• 13:55Speaker 02

  There's actually another problem that's bigger. I'll answer your first question, but then I'll address the other question that's actually more on my mind. So in the lab, you're often relatively limited to the resources you have. You have maybe a couple of grad students and a few laptops or something like that, right? Like these days, maybe you have a bit of cloud, but you don't really have that sort of resources you would have. So it turns out there's not been a lot of science, but the science is really interesting and growing on how to distribute formal reasoning. So there's a thing, for example, called Malloved Mono, where they distribute propositional satisfiability solving. It's really powerful. And if you have a cloud scale, like a team to operate a cloud service,

• 14:34Speaker 02

  and you have the sort of resources you have at AWS to run big machines, then suddenly, actually, it's much, much faster. So the performance of the reasoning isn't the big gotcha, and it's getting faster and faster, and I'm not worried about that. What is a problem, though, is scaling the... So whenever you're doing reasoning about systems, you A, have to articulate what you want to hold of the system. Like, is it all data at rest is encrypted? Is it we never log credentials? Is it like what property do you want to hold of the system? And you have to do that in a way where you get the details right, and you have to do it in a relatively rigid setting. You have to like use a temporal logic or something like that to express it. There's a very limited number of people who can do that. And then the other piece is that you have to be tasteful about what you're not going to prove, right?

• 15:18Speaker 02

  You're not going to go and prove the correctness of the language runtime, the compiler, the microprocessor, the program is running on. So you have to basically build assumptions that the reasoning relies on and making those decisions and articulating those. It's a lot about how do you do the encoding such that the tools work? And again, that's a fairly small set of people who can do that. So I'd say the big challenge, oh, and then culturally, your average person who knows about formal reasoning is not going to be very Amazonian, if you will. Right? There's a big cultural gap between people who are relatively rigid logic. When they looked at a lot of opportunities in the world, they said, no, I'm going to do mathematical logic instead. So what interests them and what drives them is really different than what you're going to find with a person who would join Amazon because they're interested in the cloud or other dimensions.

• 16:03Speaker 02

  So culturally, they're a little bit different. And so bringing all those pieces together, finding a manager who can run scientists who understands Amazon, but also understands the science community. And then another big one is finding people who can drive the tools or who can do the encoding. And thankfully, the problem around the encoding is with AI tools these days actually is getting dramatically easier. So with the idea of neuro- symbolic AI, where you combine formal reasoning with the neuro-inspired techniques like transformer models, suddenly you have ideas of auto-formalization and like, there's a whole bunch of new building blocks that we can use to really scale this activity out. And so that's actually turned out to be tremendously helpful quite recently.

• 16:43Speaker 01

  Yeah, I wanted to get into the neuro- symbolic AI, which you mentioned there. But I guess like for the audience that's probably not, you know, super familiar with it. Like, what is sort of the definition of that area? Is the neural essentially just you're leveraging LLMs in this case? And that kind of is serving as the neural layer? And then you're combining that with sort of more traditional symbolic reasoning?

• 17:05Speaker 02

  I mean, you're probably going to pull five experts in the area and they're probably going to argue about the definition. But broadly speaking, in my mind, it's the combination of a symbolic where you're pushing symbols to represent the infinite. You're like, X less than Y is the set of all pairs of. Of integers, if you will, such that the first is less than the second, right? So that's an infinite set. So when you begin talking about formulae with variables and you're sort of pushing symbolic formulae, you're doing symbolic reasoning. So that's the symbolic of neuro symbolic. And then the neuro is these, yeah, these sort of, I mean, L L M's is absolutely the classic. That's the big hot thing right now, right? For sure. But more statistical or Bayesian thinking. And then when you combine them, you can get, depending on how you combine them,

• 17:50Speaker 02

  you get different advantages and disadvantages. And so it kind of depends on, you can use formal reasoning as to synthesize training data to make your language model, for example, much more powerful. So actually, a lot of model providers do that today. They use the lean theorem prover, for example, and synthesize a lot of true and false theorems. And then we'll train over that data. And then you'll find that the language model is actually better at like recipe design and so on. And then the other extreme is you could sidecar a formal reasoning tool on the output of a language model. And then either ask the language model to express it in the formal language or do some sort of translation. That's kind of the other extreme. And then there's sort of middle grounds where you try and integrate symbolic reasoning into the inference procedure itself. And that does that, you see a lot more of the two extremes and not as much in the middle right now.

• 18:36Speaker 01

  I mean, from a, I don't know, big picture perspective, if you're trying to achieve AGI or something like that, it seems like you would need at least both sorts of approaches where L L M's are very good at a certain class of problems. And then sort of these more formal reasoning, things that you can define as correct, are going to be best sort of used for a different class of problems. They're kind of complementary. So if you can put them together, it feels like that would be a necessary step to reach some sort of more general intelligence across like a variety of different problem sets.

• 19:05Speaker 02

  I'm very much an armchair cognitive scientist, right? I'm not, I'm not a practicing one. So I'm, I am a specialist in my sort of branch of AI, if you will. So you'll want to take what I say with a grain of salt. But I like your characterization that it's a necessary but not sufficient condition for whatever AGI means, but like breathtaking AI. That's hard to know if this is a human or not. I would think you need both logical and the transformer type stuff. The thing I'll say is that For years, the propositional satisfiability solving, right, is this classic NP complete problem. The tools for propositional satisfiability solving have far, far, far exceeded human capability, like years and years and years ago, and they get better and better and better.

• 19:46Speaker 02

  So like you can take the entire design of a nuclear power plant or a railway switching or whatever, and with millions of variables, millions of connectives, ands and ors and so on, and show there are no satisfying assignments or find satisfying assignments in those spaces. And like you could collect the entire humanity and ask them to solve it, and they wouldn't be able to solve it in that time. So it's like, in a sense, it's like far exceeded human capability long ago. But they were extremely brittle to use, right? To get the answer required you to understand logic. And then if you go to like a satisfiability module, a theory solver, a lean or Isabel, these kinds of tools, you needed even more and more expertise just to ask your question.

• 20:29Speaker 01

  Yeah.

• 20:29Speaker 02

  That was typically the real bottleneck for you.

• 20:31Speaker 01

  Yeah, so there's pairing that with an LLM where you can have like a natural language interface in these that I assume significantly sort of democratizes the access to it.

• 20:40Speaker 02

  Yeah, there's all kinds of tricks you can pull now. Like you can call a language model multiple times to do translation from natural language to logic. And then you can use a theorem prover now to prove equivalence of the different attempts. So the more you do that, so the more confident you get, you got the translation, right? And then now you can, once you've got that into a formula, you can walk the formula. Like you can use the propositional structure or the logical structure in the formula to identify interesting corner cases and then articulate them back in natural language. So you can help someone who doesn't understand logic know what the formula is saying. And then you can go from natural language to logic. And then now we've got those pieces of equipment. There's just so much you can do around, like if you're agentic workflows, if you're ruling out bad behaviors from agents,

• 21:25Speaker 02

  and then you decide later on you don't like the formula that describes the safety range, you can then modify that formula and then go replay all the agentic actions and see what would have happened and just all kinds of stuff you can do that wasn't possible before.

• 21:38Speaker 01

  Yeah, I mean, given that historically the hardest part of some of these formal methods was kind of like the human bottleneck of writing the specs. How is this transforming some of the, even the things where you found success in previously at AWS around the sort of formal verification around policies and things like that? Is it changing that kind of work as well?

• 21:58Speaker 02

  So one choice we made when I started the automated reasoning group, I remember it was like Ken McMillan as another scientist in my space. I was just before I joined Amazon, I had told him I was going to join Amazon and I was having coffee with him and he joked, man, I'd love to get out a program verification. And so when I, actually that idea stuck with me. So when I joined Amazon, the policy reasoning and the network, like VPC reachability analyzer, that's an AWS product, and IMXs analyzer, or S3 block public access, those are all based on, on these tools that actually combinatorial reasoning. So they're actually, they are decidable, they're not undecidable. And so there, the real trick is to do combinatorial reasoning and there the tools are like propositional satisfiability or satisfiability modular theory solvers, and they're just unbelievably fast and

• 22:43Speaker 02

  no LLM will ever beat them. But what the LLMs do now is they actually call those tools. And so that hasn't really changed. What has changed is reasoning about programs. Because now if you have loops, right, and you're now worrying about termination of the loops, or you're worrying about finding an inductive invariant of the loop, or you're worrying about concurrency, so you're looking for rely guarantee constraints. Now, the algorithms, the procedures that existed before were pretty brittle. And now you can just ask the LLM, when the LLM's writing the code, you can just say, can you find the inductive invariant for me at the same time? And it does a pretty good job. And then what we've seen with recent advances in the models, like in the past year, is like really breathtaking. So we,

• 23:27Speaker 02

  whereas before we had five humans who could drive these theorem improvers, those humans are now really excited because they're able to let the models go and do the proof search for, like agentic tools, go find the proofs for them and they run like thousands of these jobs at the same time. So we're getting like, it's not only like 10x or 100x, it's like 1000x productivity gains from that small seed of individuals who can drive these things. And the amazing thing is because these tools like Lean theorem improver, they are yes or no tools, right? You can pass them very complicated things and they will say yes or no. It's like the scaling is unbelievable as opposed to, I don't know, poetry or other areas where the yes, it's not as easy to say yes, no.

• 24:07Speaker 01

  So it seems like there's a couple of different, or there's a spectrum of approaches where you could combine like an LLM or reasoning model with these kind of formal methods where it's like, you know, verifying AI output, or even some of the stuff that you, where the LM can rely on the formal method and sort of trigger that to handle certain sort of logical reasoning problems, or even using AI to make the formal methods easier to use and sort of democratize the answer. So I go, out of those, that spectrum, like what part of that I think excites you the most? Like, where do you see the most opportunity?

• 24:38Speaker 02

  Well, I mean, there's just nothing but open field for the opportunity. Actually, all of them. It's just absolutely unbelievable. I just really didn't think it would happen in my lifetime that previously, you know, I had like four or five friends of mine who had worked with in the past in different institutions, and I brought them to Amazon, and basically their job was to sit at a terminal and drive these tools, and they were the neuro, right? They had read all the proofs and understand all the tools, and they could run these things. And suddenly, it's just like you get kind of unbelievable capacity from them. So I just, I actually don't see a ceiling for that productivity. The thing that I'm probably most interested in intellectually is agentic safety.

• 25:17Speaker 02

  To, I think of agents as allowing us to scale things that where we only had socio-technical mechanisms before. So now you have a choice of socio-technical or these kind of agentic tools. And there's a disadvantages, advantages to them, right? So

• 25:31Speaker 01

  What do you mean by socio-technical?

• 25:33Speaker 02

  So a socio-technical mechanism is a mechanism where you are inserting people at certain stages as a protocol to raise the bar or make decisions, right? So like the police is a socio-technical mechanism, right? You, I don't want to go to jail. And so therefore, there are certain things I won't be doing because I don't want to go to jail and right? And my employer can call the police, right? So whereas agents aren't afraid, they don't fear jail whatsoever.

• 25:58Speaker 01

  That might be the actual responsibility of the engineer at this point. Like if the AI is writing the code, you can't send the AI to jail, but you can send the person who sent the instruction to jail, basically.

• 26:08Speaker 02

  Right. So that's where this formal stuff comes in, right? So if now what we're doing is if we ask the human to look at the output, if we say, hey, you're responsible. Before the output always, in some sense, you haven't really scaled the person and now they're just going to hit cognitive overload. Imagine they have like a thousand agents writing code on their behalf and their entire job is just to read the output of agents. They're going to miss things for sure. So what you really want is you want to actually write down. Whereas maybe we weren't before because there wasn't, there wasn't an advantage to doing it. Actually write down what you want to hold. So what is availability? What is confidentiality? What is integrity? What is privacy? What is sovereignty? What is durability? What are these concepts and can you write them down in a linear temporal logic or computational tree?

• 26:51Speaker 02

  You know, C T L. What is the formalism for which you would want to express these things? And then can you use these auto formalization techniques to get them right? And then now can you, in an agentic execution environment, before allowing the commands or programs that have been synthesized by the agents L L M, allow them to go execute? Can you now go statically check that those things won't violate the confidentiality, integrity, durability? You know, availability rules and then allow to go. And if you can get that right, then now agents just become unbelievably powerful for us. It's a very humanistic view because it's still, it's still saying, it's a more declarative programming model.

• 27:31Speaker 02

  Right? You get to say, you know, we in natural language in a room can decide this is what availability is. This is what integrity is. This is what confidentiality is. And then if things happen in the future that we don't like, then we can refine that definition together. And then one could imagine best practices where they're open source and like, oh, this is what these other enterprise organizations use for confidentiality. We should copy those. And then we can, for compliance, we can now talk to the auditor and say, well, here's our definition of confidentiality. And so then I think really it sort of unlocks a lot of a scaling dimension that's just would previously unheard of.

• 28:05Speaker 01

  So the first problem is that if everybody's running, you know, a ton of different agents, like at some points, people are going to miss something because they're context switching all the time. If you're doing this for engineering, you're spinning out a ton of code. There's no way you can, you know, hand review every single line of code and make sure that it's right. And even if you did, you still might make mistakes. But now you're sort of shifting some of that problem to trying to do, like spec this out beforehand in terms around like what the expectations are. But Are you sort of shifting that problem to you? You kind of have to be able to predetermine all the the situations where the agent might get itself into trouble, right? So how do you start to like formalize that? And also, I guess, like, bound that problem down to something that doesn't take forever to essentially define?

• 28:50Speaker 02

  So the answer is yes. And there's a quote that's I like this related. So Einstein apparently said, everything should be as simple as possible, but no simpler. So yeah, ultimately, we are still having to decide as a society or as a leadership team or as a as a family, what's allowed and what's not allowed. And actually, organizations at scale tend to articulate these things out, right? Amazon, we have the leadership principles, and that really helps Amazon scale a lot. When I'm going through an uncertain time, or, you know, something's happening and I don't, I can't just go call my boss every time I'm confused. How am I making those decisions? I rely on the leadership principles to give me guidance. And, you know, in an agentic setting where you don't have human judgment, you will want to be rather more concrete, but then you can use symbolic

• 29:34Speaker 02

  formulae to describe the infinite set of things you're okay with and not okay with. And then using that the formula, you can then find the interesting witnesses of what's allowed and not allowed to show them to a committee, to the society, to a leadership team or to a family. These are the kinds of things that will be allowed or not allowed. How are you feeling about that? And kind of run those things ahead of time. I think you can't make it simpler than that. You ultimately do want humans to set the policy on kind of what is the context in which we're going to let agents just rip? And what are the boundaries for which we don't want them to cross? For like, you know, we don't want them to send money to certain countries or buy certain kinds of stocks. And I think

• 30:16Speaker 02

  it's an exciting opportunity. I think it is the sort of scaling that you got glimpses of in really large, successful organizations, but it's kind of a way of thinking that a lot of people haven't thought about before, but it's but it's an opportunity now that for for scaling yourself, but your family and organizations.

• 30:33Speaker 01

  So a lot of times in, you know, either whether you're a model provider or you're building some sort of agent system, you'll use things like the system prompt to put in certain guardrails around like, hey, like this agent should be able to answer certain types of questions. So this sounds like a more sort of formalized version of that where it's not just about the formalization of the spec, but also when the agent does something, being able to go back to the spec and essentially check in a formal fashion, whether you're allowed to do that thing or not. Is that a fair characterization?

• 31:06Speaker 02

  Yeah. So my mental model is definitely answers for which there are right or wrong answers, right? Like on Family Medical Leave Act or New York City Department of Buildings, there are questions for which like, no, you are not allowed to put the air conditioner there. Or, you know, like you in a two-family building, you do need sprinklers. But there's all kinds of like, when you look at the codes, it's like the conjunction of codes from different years and often this kind of conflict between them. And so often these kind of rule systems that we have in society often conflict. And so now's a really great time to find all those things, identify the conflicts, decide on the answers in a fair and equitable way around what are our answers going to be? And then allow agents to take action or humans to take action.

• 31:49Speaker 02

  But I definitely have in my mental model, those questions for which there are right or wrong answers. Like, should we send this money to here? Does this violate your tax strategy? Those are right or wrong answers. And then there's stuff that's more like, you know, is that a bad thing to say? Is that a bad word? Or like these things are a little more on the statistical spectrum. And I think that you could probably use some of these same mechanisms, but that's, I have a harder time wrapping my head around, like, is this a good poem?

• 32:16Speaker 01

  I think that's the hard part is the things that are subjective. I've actually, I've written a little bit about this where I think one of the reasons why we see such success in engineering sort of really being the tip of the spear with not only agents, but models in general is because when you code, you have a lot of built-in guardrails in terms of whether something works or not. Like there's deterministic ways, like you could, if you generate code, you could compile it, you can run it against tests. Are some form of verification of whether there's correctness behind what you've generated. But if I'm generating a poem or even, you know, I don't know, a press release about a product launch, like the quality controls are much more subjective and it's hard to essentially put some sort of formal verification around it

• 32:59Speaker 01

  to determine whether it's good or not. And then the feedback loop in engineering is also very fast where you're, you could, you know, compile it, pass the test, even run it. And then if errors happen, feed the error back into the system, self-correct and generate new code and do that in essentially a loop. But it's hard to do that in a lot of domains because by the time you know something's wrong, the space between generation and knowing it's wrong could be a really long period of time.

• 33:24Speaker 02

  Yeah, I agree. I think I'm fortunate to be working on the side of the spectrum I'm on because I'm just enjoying huge benefits. Whereas in music or poetry, it's harder. I will say that there is a boundary that's not 100% clear and there's probably pretty exciting work there. It'll be more statistical in nature. You'll be like, I'm relatively confident that this discussion, even if it's translated into like some like Vulcan or some, you know, some language that's not natural, that's not English or something like the argument that would be made still ultimately roots out to chemistry and then chemistry is a formal system. So I think in some applications, there's, if there's a formalism hiding down somewhere, then there's probably something we can do using this. But yeah, I mean, for, for me, it's on mathematics

• 34:09Speaker 02

  or reasoning about correctness of programs or reasoning about policies or security. It's like, we're well on the side of the spectrum that we're, we're happy about.

• 34:18Speaker 01

  Yeah. And I think a lot of probably B to B type enterprise problems fit into that class structure versus the just open-ended kind of, you know, you ask anything and get any possible answer.

• 34:28Speaker 02

  Yeah. The addressable market for answering questions about correctness according to law and tax strategy across like agentic financial systems is so big that it's worth going after. Even if we can't answer questions around a poem being a good poem.

• 34:48Speaker 01

  Yeah. Healthcare probably similarly is, right?

• 34:51Speaker 02

  Yeah.

• 34:51Speaker 01

  So with an agent, there's going to be. At least sort of two big safety concerns or trust concerns with those. One is that the agent might take action or access data that shouldn't or is unexpected. And then also it could hallucinate some answer to some question or something like that. That also leads to a misleading result. So is what you're talking about possible to kind of potentially address both of those problems? Or does it bias towards one more than the other?

• 35:21Speaker 02

  So in the space of like, you know, chatbots or that kind of thing. We have, we have a product called automated reasoning checks and bedrock guardrails. It helps you formalize your domain, like, you know, family medical leave act or your vacation policy or your travel policy. And then in an inference time setting helps you remove incorrect statements and only produce correct statements and can explain why the answers are correct. So, and that allows it not only for you to remove incorrectness due to hallucination when you're dealing kind of with your customers, but it also allows you to understand your rules. Because there may be cases where your rules were wrong and the customers are like, that can't be right.

• 36:04Speaker 02

  And so you can use the feedback from the customers to identify actually where you, we got things wrong, which is actually fairly common when people kind of bring their policies and from the text file to now being used in an LLM based situation. On the other one around basically where like we regularly analyze using automated reasoning tools and entire AWS services, looking at where data flows to and from. So we can, we can track, you know, we don't track the data itself, but we can track the flows being using statically analyzing both code and the infrastructure of AWS to show where our data flows to and from. And then that allows us to make pretty high fidelity decisions around risk,

• 36:48Speaker 02

  around what information we're using to make decisions. And so I think that's an area that the broader IT community can use too, right? If you're building a Gentic generative AI based solutions that plugs into databases, data lakes.

• 37:03Speaker 02

  You know, these kinds of things, you can analyze your service and determine where data is flowing to and from. And then if there's certain pieces of information that shouldn't be contributing to the answers, say in a medical domain, like if you don't, if you don't want the agent to leak other customers. PII, for example, then that's the sort of thing you can establish and maintain as an invariant using the automated reasoning tools.

• 37:25Speaker 01

  So one of the things that you said earlier was that, you know, there's only, you know, maybe two or three thousand people that kind of specialize in this area of automated reasoning. And it seems like in recent years, automated reasoning has kind of broken somewhat into the mainstream. I guess like, why now? Like, what has changed in particular for this to suddenly have sort of more visibility as an area that's important for, you know, building successful software?

• 37:50Speaker 02

  I'll give you this short term answer and then as I show a little bigger context. So, I mean, it's agentic AI. Like, you know, 10 years ago, if I had described what I did on a podcast like this, I think most people, very, much smaller set of people would track even what we're even talking about. And I think what's really amazing about generative AI is that as a society, we're going through an exercise, a sort of art of the possible exercise, right? There were tools that use natural language that were very easy to call, you just went to a website. And people are like, oh, wow. And they sort of realized that computers could answer questions, very deep questions and reflect and so on. They weren't always right, but they could do it, right? And so then it's a small delta from that to like, how do I make sure these answers are correct? Which is kind of what automated reasoning has always been sold.

• 38:32Speaker 01

  Right, yeah.

• 38:32Speaker 02

  But before you were trying to talk about, imagine a computer could tell you and they're like, I don't even know what you're talking about, right? Like, so we just out of the gate, the presupposition of the work was just like lost on the vast majority of people. So it just wasn't, it didn't click for people. And so like, it was a very small set of people whose brains were sort of like wired for to be interested in that problem. And that's, so then people just kind of self-selected. So I, so I think that has changed. The bigger picture is that, you know, like. The inventors of computing were all formal methods people, right? Like Alan Turing wrote a paper called Checking a Large Routine, which shows you how to prove the correctness of a program. And von Neumann was a proof for the all these, all these people from the 1950s and 40s were mathematicians who knew how to do proofs.

• 39:15Speaker 02

  And very clearly in their mind, they understood that programs mapped to Turing machine. Turing machines are like automata. So like it was abundantly clear, it was like not even worth mentioning.

• 39:24Speaker 01

  Yeah.

• 39:25Speaker 02

  And it was kind of only when the IT industry, like when computers became like commercial mainframes and then mini computers and so on, that the branches of the mathematical view of, of programs and how to reason about programs. And then the sort of IT industry kind of divided. And so you'd meet people kind of didn't like you'd, you meet formal reasoning experts, particularly in Europe, who have like never written a computer program in their life. They don't know how computers work, but they understand the mathematics of Turing machines. And then on the other hand, people who write computer programs all their life, but don't even know it's possible to prove correctness of programs. So the, the worlds have kind of divided. And then in AI, you saw the same thing, right? So AI, like one of the first applications of, when the first IBM commercial computers was actually to automate the reasoning from Principia Mathematica.

• 40:09Speaker 02

  Right? So automated reasoning was one of the first non-military applications of computers. And then AI, John McCarthy coined the term AI. He was a formal reasoning person. So in, in the very beginning, AI was sort of the mixture of these like Bayesian cognitive, logical, the mix of those ideas. And people were very excited and it was very heady days. But then you had this sort of series of AI winters where government funding would dry up for these areas. But the response was for people to get much rather more specialized. And so what happened is automated reasoning folks, like the people in the logical view, found very niche applications that they could solve with their kinds of tools. And we're successful there. And that's kind of where I, how I grew up.

• 40:50Speaker 02

  And then other people went to, you know, recognizing numbers for depositing checks. And so there was another set of applications for which some of the other techniques were going to work better. And so the areas kind of grew apart. And what's happened with generative AI and now agentic AI is that the money, but also the, you know, the disruption, the opportunity has really kind of brought all the communities, the communities are kind of coming back together. And there are. Certain members of the of the those crowds that are bilingual that can talk between all those communities and they're just worth their weight in gold. So.

• 41:23Speaker 01

  Yeah, it's interesting. I think this whole area is bringing back a lot of things that have had, you know, periods of time where they were, you know, there was like a big research backing behind it. I think like ontologies certainly have been something that I, and you know, I did my PhD in the knowledge engineering space with ontologies and worked on ontology mapping problems. And then, you know, no one was talking about that for like a decade. And then now it's come back in a big way. There's all, there's a bunch of different things and even in distributed computing as well, where if you have agents that are making all kinds of network calls, you're going to run into distributed systems problems. And that's really, I think, brought to the forefront, the idea of like, you know, durable execution and durable functions and all this type of stuff that historically has been a little bit more, you know, niche. Certainly companies invested in that, but it wasn't like

• 42:08Speaker 01

  everybody's problem. And now suddenly it's like everybody's problem.

• 42:11Speaker 02

  At Amazon, it's funny because you know, like sometimes, you know, very big names will join Amazon and they'll hear about the automated reasoning and be like, oh, we tried that at my, you know, like company 20 years ago didn't work. And we're like, well, you know, maybe you should be maybe that was 20 years ago. So like things change. And I think it's like music, you, you see ideas like old ideas influence or fashion, right? Things come back and they get integrated in different ways. And so, yeah, so pendulum swing, ideas go out of fashion, come back into fashion. And it's, it's actually frankly, good because I think it's good. It's good to get a mixture of ideas and people confused about them. And some people really advocating for some and some people advocating for other and then finding combinations in that. I think it gives diversity of thought, which I actually think helps us solve problems in better ways. So it's pretty exciting, actually.

• 42:55Speaker 01

  Yeah, absolutely. I mean, I think sometimes someone with a different perspective can break through in a problem area that in a new way that no one's ever really considered before because the people who work in that area are kind of like locked into a certain way of thinking.

• 43:06Speaker 02

  Totally. Like, yeah, if you had put me on that speech to speech translation problem with mathematical logic, I would have never gotten anywhere. But I would have kept insisting I had the right way to do it, right? I would have been like, give me another year, give me another year. And I absolutely would have never solved it.

• 43:20Speaker 01

  Yeah, it would have just kept hammering that nail and it would eventually go. For software engineers that are, you know, listening and interested in starting to apply automated reasoning or learning more about it, like where they begin, like what tools, you know, I don't know, books, practices, would you kind of recommend for them?

• 43:37Speaker 02

  The ground is moving kind of under our feet. So the advice I would have given a few years ago is actually a little bit different than what I give right now. We've open sourced something called Strata, which is a intermediate representation for programs that allows you to represent Python and allows you to represent, you know, Java and Rust and so on. But it unifies to the logical representation, which ultimately the semantics are something called Lean. So Lean, there's a theorem prover called Lean. There's many theorem prover, you know, Anarcho theorem prover, so Isabel, Hallite, Lean, so on. But Lean is the one that many mathematicians have sort of clicked to. So that's the, becomes the lingua franca for them. And because of language model

• 44:19Speaker 02

  training, so language model providers discovered this data and began training over it and saw the value of this data. So then they've now begun to synthesize data using Lean. So for example, DeepSeek did that. Reinforcement learning together with Lean is a very powerful concept. Yeah. Lean is kind of become a relatively standard tool in that space. So I would go use Lean. It's a mathematician's tool and it requires you to, traditionally to hold its hand. It's not, it's automated reasoning is a sort of, almost a misnomer, right? It's like, very far from automated. I mean, it automates the checking of the argument you found, right? Whereas these tools like a propositional satisfiability solver like Cattle is fully, fully, fully automated. But it's only

• 45:02Speaker 02

  solving the combinatorial problem, whereas Lean is solving an undecided, is trying to solve an undecidable problem with your assistance. But what's really amazing these days is, you know, like the language models are really good at running these tools. So if you have Lean together with a language model, now you're in business. Now you can do some really interesting things. And so if you want to reason about programs, one way to do that is to translate the programs from Rust into Lean via Strata, which we've open sourced, and then to reason and Lean. And then one could imagine, you know, products are coming, there's startups and then AWS, we're all, we're all kind of building products in this space. So there will be various products and, you know, I'd love for people to use AWS ones, but there's, there's other startups that are building stuff too. So.

• 45:47Speaker 01

  Yeah, I mean, that's amazing. I think that's one of the things I'm most excited about in terms of like, I don't know, these days that we're living in right now is sort of the accessibility suddenly to all these different areas. You essentially have a way to get access to information that you've never had access to. It reminds me of like, you know, when I was a teenager and the internet became, you know, something suddenly did not have to go to a library to look up, you know, every information and just be able to look that up on the internet. Even those early days where there's a lot less websites and stuff like that was just amazing and really opened up the world for me at that time. And I think we're seeing that again.

• 46:20Speaker 02

  Totally. Yeah. When I look at like, you know, I used to work on Volkswagen motors, like air cooled 1960s. When I was in high school, that's what I did. And the things I had to do to learn how to fix problems when I didn't know what I was doing was are amazing. Right. And then when I look at my son and how he can use online videos to learn how to use equipment, music equipment. So it's incredible. And then the the language models are just like another step forward. It's pretty incredible.

• 46:47Speaker 01

  Is there anything else you'd like to share?

• 46:49Speaker 02

  People should follow me on LinkedIn. I try and post if they're interested in stuff they're hearing here. I post, you know, try and post just a few things, but they should be of kind of interest to people who are tracking formal methods. So I'm Byron Cook. Yeah, I don't know. Probably not. No, I'm just keep doing it.

• 47:06Speaker 01

  All right. Yeah. Byron Cook. I'm gonna follow you right now. There we go. Awesome. Well, thank you so much for being here. I really enjoyed this. This was fantastic.

• 47:13Speaker 02

  Yeah, it's a pleasure. Thanks for your time.

• 47:15Speaker 01

  Cheers.