Formal Methods as Agent Guardrails

23:50How 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? So one choice we made when I started the automated reasoning group, I remember I was like Ken McMillan as another scientist in my space. 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 IM access analyzer or S3 block public access, those are all based on these tools that are actually combinatorial reasoning.

24:33So 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 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 over the loop, or you're worrying about concurrency, so you're looking for rely guarantee constraints.

25:08Now 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 whereas before we had five humans who could drive these theorem provers, 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.

25:47So we're getting like, it's not only like 10X or 100X, it's like 1000X productivity gains from that small seat of individuals who can drive these things. And the amazing thing is because these tools like Lean Theorem Proover, 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 or no. 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 where the LLM 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 democratizing.

26:35Out of that spectrum, like what part of that, I think excites you the most? Like, where do you see the most opportunity? 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 I'd worked with in the past and 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.

27:06And suddenly it's just like you get kind of unbelievable capacity from them. So I just actually don't see a ceiling for that productivity. The thing that I'm probably most interested in intellectually is agentic safety. I think of agents as allowing us to scale things that were we only had sociotechnical mechanisms before. So now you have a choice of sociotechnical or these kind of agentic tools. And there's disadvantages and advantages to them, right? What do you mean by sociotechnical? So a sociotechnical mechanism is a mechanism where you are inserting people at certain stages as a protocol to raise the bar or make decisions, right?

27:46So like the police is a sociotechnical 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. That might be the actual responsibility of the engineer at this point. 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. 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 for the output always, in some sense, you haven't really scaled the person.

28:24And 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 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? Can you write them down in a linear temporal logic or computational tree, CTL?

28:56What 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 agent's LLM, allow them to go execute, can you now go statically check that those things won't violate the confidentiality, integrity, durability, availability rules, and then allow it 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 saying it's a more declarative programming model.

29:35You get to say, 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 sort of unlocks a lot of a scaling dimension that's just previously unheard of.

30:09So 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 spitting 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 kind of have to be able to predetermine all the situations where the agent might get itself into trouble, right?

30:46So 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. So the answer is yes. 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 family, what's allowed and what's not allowed. And actually organizations that scale tend to articulate these things down, right? Amazon, we have the leadership principles and that really helps Amazon scale a lot.

31:17When 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 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 formulae to describe the infinite set of things you're okay with and not okay with. And then using 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.

31:57These 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, we don't want them to send money to certain countries or buy certain kinds of stocks. And I think it's an exciting opportunity. I think it is the sort of scaling that you've got glimpses of in really large, successful organizations.

32:27But it's kind of a way of thinking that a lot of people haven't thought about before. But it's an opportunity now for scaling yourself, your family and organizations. So a lot of times in 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.

33:09Is that a fair characterization? 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 there's conflict between them. And so often these kind of rule systems that we have in society often conflict.

33:40And 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 our answer is going to be, and then allow agents to take action or humans to take action. 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.

34:13And I think that you could probably use some of these same mechanisms, but that's, I have a harder time wrapping my head around, you're like, is this a good poem? 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 if you generate code, you could compile it, you can run it against tests.

34:47Those are some form of verification of whether there's correctness behind what you generated. But if I'm generating a poem or even, 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 to determine whether it's good or not. And then the feedback loop in engineering is also very fast where you could 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.

35:18But 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. 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.

36:00And 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 me, it's on mathematics 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 happy about. Yeah. And I think a lot of probably B2B type enterprise problems fit into that class structure versus the just open-ended kind of, you ask anything and get any possible answer. The addressable market for answering questions about correctness according to law and tax strategy across 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.

36:52Yeah. Healthcare probably similarly is, right? Yeah. 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? So in the space of like, you know, chatbots or that kind of thing, we have a product called automated reasoning checks and bedrock guardrails.

37:34It 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 like that can't be right. 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 in from the text file to now being used in an LLM based situation.

38:23On the other one around basically where we regularly analyze using automated reasoning tools and entire AWS services, looking at where data flows to and from. So we can track, you know, we don't track the data itself, but we can track the flows using statically analyzing both code and the infrastructure of AWS to show where data flows to and from. And then that allows us to make pretty high fidelity decisions around risk, 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 agentic, generative AI-based solutions that plugs into databases, data lakes, you know, these kinds of things, you can analyze your service and determine where data is flowing to and from.

39:12And 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 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. 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?

39:44Like, 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? I'll give you the short term answer. And then as I said, 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, a 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 sort of art of the possible exercise, right? There were tools that used natural language that were very easy to call.

40:19You just went to a website and people were 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. Right. Yeah. 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.

40:48So 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 to be interested in that problem. And that's – so then people just kind of self-selected. 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 – all of these people from the 1950s and 40s were mathematicians who knew how to do proofs. And very clearly in their mind, they understood that programs mapped to Turing machines or like automata.

41:25So like it was abundantly clear. It was like not even worth mentioning. And it was kind of only when the IT industry and like when computers became like commercial mainframes and then mini computers and so on, that the branches of the mathematical view of programs and how to reason about programs and then sort of IT industry kind of divided. And so you'd meet people who kind of didn't like you'd 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.

41:54And 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 worlds have kind of divided. And then in AI, you saw the same thing, right? So AI, like one of the first applications of one of the first IBM commercial computers was actually to automate the reasoning from Principia Mathematica, 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 the very beginning, AI was sort of the mixture of these like Bayesian, cognitive, logical, the mix of those ideas.

42:32And 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. The response was for people to get rather more specialized. And so what happened is the automated reasoning folks, like the people in the logical view, found very niche applications that they could solve with their kinds of tools and were successful there. And that's kind of how I grew up. 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.

43:04And 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 those crowds that are bilingual that can talk between all those communities and they're just worth their weight in gold. So, 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.

43:36I think like ontologies certainly have been something that, 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.

44:10Certainly companies invested in that, but it wasn't like everybody's problem. And now suddenly it's like everybody's problem. 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 reason and be like oh we tried that at my you know like company 20 years ago it 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 our fashion right they 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 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.

44:52It gives diversity of thought, which I actually think helps us solve problems in better ways. So it's pretty exciting, actually. Yeah, absolutely. I think sometimes someone with a different perspective can break through in a problem area 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. 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.

45:20I would have been like, give me another year. Give me another year. Yeah, absolutely. Would have never solved it. It would have just keep hammering that nail and it would eventually go ahead. 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? 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'd give right now.

45:47We've open sourced something called Strata, which is a intermediate representation for programs that allows you to represent Python and allows you to represent Java and Rust and so on. But it unifies to the logical representation, which ultimately the semantics are in something called Lean. So there's a theorem prover called Lean. There's many theorem prover, interactive theorem prover, so Isabel, Hall-Light, Lean, so on. But Lean is the one that many mathematicians have sort of clicked to. So that becomes the lingua franca for them. And because of language model training, so language model providers discovered this data and began training over it and saw the value of this data.

46:28So then they've now begun to synthesize data using Lean. So for example, DeepSeq did that. Reinforcement learning together with Lean is a very powerful concept. Lean has 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. It's 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 Catacol is fully, fully, fully automated.

47:05but it's only solving the combinatorial problem. Whereas lean is solving an undecided. It's 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 a 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.

47:40There's startups and then AWS. 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 other startups that are building stuff too. So, well. Yeah, I mean, that's amazing. I think that's one of the things that 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.

48:17Even in 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. 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 were 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 language models are just like another step forward.

48:49It's pretty incredible. Is there anything else you'd like to share? 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. All right. Yeah, Byron Cook, I'm going to follow you right now. There we go. Awesome. Well, thank you so much for being here. I really enjoyed this. This was fantastic. Yeah, it's a pleasure. Thanks for your time.

49:19Cheers.

49:31you