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 and force 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 I Am 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. This episode is hosted by Sean Falconer. Check the show notes for more information on Sean's work and where to find him.
Byron, welcome to the show. Thank you very much. Thanks for having me. Yeah, absolutely. We're looking forward to this. So we're going to probably cover a lot of ground today. You've had a pretty rich history, but one of the things I want 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? This is a lot of jobs to balance. How do you manage wearing those three different hats simultaneously?
Cognitively, the same job. 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 that 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 find the right people at the right tools to prototype something and then simultaneously write some sort of report or some sort of PowerPoint document or something in the language of the institution to help them appreciate what's possible 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 in Amazon, I'm at any given time, have three or four things going on, some sort of context switching between those things. Anyways. Was that something that you're always interested in trying to tackle these types of problems that seem impossible?
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 on working on cars or doing music or these kinds of things, people sort of 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 3000 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. 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 or the particular details of the organization don't really matter. I'm just usually being the place that sort of the best place for me to be and to help the community figure out how to solve problems.
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. I said we built a tool that could automatically prove whether certain types of programs can terminate and making a significant contribution to the halting problem. I guess like what made you believe that something like that was solvable given that I think like eventual wisdom and even now in touring said otherwise. 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 restrictions always has to give an answer will be okay with maybe the tool not giving 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 journal and touring is fundamental and absolutely staggering. But on the other hand, there's lots of things that are unsafe that we do all the time driving us unsafe, but we get in the car. And if we get to our destination, we know we got there safely. And so the insight around that area is really interesting. I was actually working in the Windows kernel team and I was carpooling with a person who developed in the Windows kernel team and he kept when we're talking about things that should hold up the kernel he kept using the word eventually like what this happens that should happen.
And I realized that was like, that is the termination questions like termination in the word eventually. So there's a theoretical result that connects them saying they're essentially the same thing. And so I realized that was an important problem and I begin thinking about what tools can we put together from existing pieces we already had to do something quite quickly for device drivers. And then that was successful and then that turned into reason about biological systems and it turned into reasoning about non blocking concurrency and so on. Yeah, and was the regional focus on device drivers was that partly motivated because at that time like device drivers was one of the biggest culprits of a situation in operating systems.
Yeah, so in the 1980s, if your computer crashed, you just, you know, like while it's sad you lost your little word processing document or whatever you're working on. But as we went to data centers, 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 rid of those crashes and it turned out that in the early 2000s, 85% of crashes in the operating systems were actually due to the device drivers. So it became important to work on. Wow. Yeah. Talk about that. High ROI. I guess.
Yeah. 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. And data structures they were operating over actually relatively simple. They were cyclic doubling lists. So in many ways, it was actually a slightly, it was an easier problem than the German or 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 theoretically, but we practically bypass some of this challenges around undecidability.
Yeah. So in one way, you're downing this unbounded problem, right, to a more specific class of the problem. Yeah, you can't solve the problem in generality. So you're going to have to identify niche areas where while it's still in my time out from time to time, it's not going to time out 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. So you can't to the person who's with the understanding of the niche problem to kind of understand the dynamics of the problem. So that happened again with reasoning about genetic regulatory pathways, where I was like, Oh, I see. So usually they have the shape and usually they're of the size, usually they're asking this kind of question.
So actually we could do something that 95% of times actually going to give them an answer and maybe 5% of the time it says, or I can't answer the question. Okay. So you've founded the automated reading 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? Let's see. So I had kind of exhausted. I mean, I'd written all the research papers. 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.
I actually sort of, I went and talked about a potential employers and kind of figured out which one I would want to work for. And I think that AWS is pretty happy to have me because it was pretty risk free. Right. Like I was going to join in there only hiring one person. I poured directly this as though if I think if it didn't work out, then I would imagine that would be the discussion that they were having like how risky is this higher.
And Amazon, I think that's 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 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 they 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.
Even that AWS runs critical infrastructure for millions of customers like going back to some of your work with like the drivers and sort of proving whether they can run successfully or not. Like other similar class of problems around IM policies and networking figs and things where if you mess those up, it can go really bad. Someone operating this type of infrastructure. Is there a way to actually apply some of your work to those areas? Yeah. So that's what we did. So when I first joined, I identified, you know, I went and tried about 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 heard.
The task could help on identified four or five of them hired a few of my friends and then we kind of went out for them and say, yeah, you identified two of them. So that one is reasoning about the semantics of AWS policies. Another one is the virtual networks because you get those wrong when you're never really bad day. And then we also worked on like low level code like virtualization and cryptography and we also worked on like the system's protocols. 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. 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 to make up with your ticket. Yeah, how's that work? I'm assuming like your team and yourself, you know, especially when you're essentially an IC, if I change this role until you hire some of your friends and support. You're sort of doing this as this like research project, I assume, and then maybe you're doing the proofs. Maybe there's POC involved. How do you go from that essentially to this thing running a production and serving millions of people?
So one piece of advice I got when I first started was the person was like, hey, you know, I get in the previous employers, you've gone for these moonshots, right? 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 while 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. And so 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 sort of built trust and built momentum on some of these others that we were able to come back to the bigger things and take them on again.
That makes sense. Even my experience having worked at a variety of different startups, when you kind of start a new role a lot of times, it's like, how do you build something big, but also how do you show value as to this possible? And so it's what's easier to do that with a smaller, more constrained project. And then as you build trust, people kind of believe in maybe the bigger thing and the longer term, the more memorable. Yeah, exactly.
Is there any challenges around from an engineering perspective where when you're thinking about like formal verification, 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 slowing it, how do you sort of engineer it to something that can run in production at scale? There's actually another problem that's bigger. I'll answer your first question, but then I'll address the other questions actually more on my mind. In the lab, you're often relatively limited to the resources you have. You have maybe a couple grad students and a few laptops or something like that.
These days maybe a bit of cloud, but you don't really have the 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 Melab Mono where they distribute propositional side of the slide, but it's really powerful. And if you have a cloud scale, a team to operate a cloud service and you have the 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 have to articulate what you want to hold at the system. Is it all data rest is encrypted? Is it we never log credentials? Is it like what property you want to hold at 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 use a temporal logic or something like that to express it. And 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. You're not going to go improve the correctness of the language runtime, the compiler, the microprocessor, the programmers 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 you do the encoding, such that the tools work. And again, it'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 knows about formal reasoning. It's not going to be very Amazonian, if you will.
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 there's interest in 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. So culturally, they're a little bit different.
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 neurosomolic AI, where you combine formal reasoning with the neuroinspired techniques like transformer models, suddenly you have the ideas of auto-formalization. And 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 by recently. Yeah, I wanted to get into the neurosomolic AI, which you mentioned there, but I guess like for the audience, that's probably not super familiar with it. Like, what is sort of the definition of that area? Is the neural essentially just your lettering LOMs in this case, and that kind of is serving as a neural layer and then you're combining that with sort of more traditional symbolic reasoning. I mean, you're probably going to pull five experts in there 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, like X less than Y is the set of all pairs of integers, if you will, such that the first is less than the second. So that's an infinite set. So when you begin talking about formula with variables and you're sort of pushing symbolic formula, you're doing symbolic reasoning. So that's the symbolic of neuro-symmolic. And then the neuro is these, yeah, these sort of, I mean, all of them is absolutely the classic.
That's the big hot thing right now, for sure. But more statistical or Bayesian thinking. And then when you combine them, you can get, depending on how you combine them, 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 Theron-Perver, for example, and synthesize a lot of true and false theorems. And then we'll train up with that data and then you'll find that the language model is actually better like recipe design and so on. And then the other extreme is you could side-car a formal reasoning tool on the output of the 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 stream. And then there's sort of middle grounds where you try and integrate small reasoning into the inference procedure itself.
And you see a lot more of the two extremes in not as much in the middle right now. 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 of those sorts of approaches where LMs are very good at a certain cost of problems. And then these more formal reasoning things that you can define as correct are going to be best sort of used for the different class of problems. They're kind of complementary. So if you put them together, it feels like that would be a necessary step to reach some sort of more general intelligence across a variety of different problems.
I'm very much an armchair cognitive scientist right now, but I'm not a practicing one. So I am a specialist in my sort of branch of AI, if you will. So you'll want to take what I say with the grain of salt, but I like your characterization that's it's a necessary but not sufficient condition for whatever AGI means. We're like breathtaking AI that's hard to know if this is 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 side of solving is the classic NP complete problem. The tools for propositional side of solving are far, far, far exceeded human capability, like years and years ago, and they get better and better and better. 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, and so on and show there are no satisfying assignments for fine satisfying assignments in those spaces. And like you can 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 Isabelle, these kinds of tools, you need it even more and more expertise just to ask your question. Yeah, typically the real bottleneck for you. Yeah, so does pairing that with an LOM where you can have like a natural language interface and these that I assume significantly democratize the access to it. There's all kinds of tricks you can pull now. Like you can call language model multiple times to be translated from natural language logic and then you can use a theorem, 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 a 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 somebody who doesn't understand logic know what the formula is saying and then you can go from natural language logic. And then now we've got those pieces of equipment. There's so much you can do around like if you're a gentic workflows, if you're ruling out bad behaviors from agents 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 agent actions and see what would have happened and just all kinds of stuff you knew that wasn't possible before.
Yeah, I mean, given the historically the hardest part of this formula is kind of like the human bottleneck of writing the specs. How is this transforming some of the things where you found success in previously 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 a not assigned to some of my space.
I was just before I joined him. I 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 of program verification. And so when I actually stuck with me, so when I joined Amazon, the policy reasoning and the network, like VPC reachability and why is there that's native product and I am access analyzer or that's three block public access. Those are all based on these tools that actually combinatorial reasoning. So they actually 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 LMs do now is actually called those tools. And so that hasn't really changed. What has changed is rethinking 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 a lot of guarantee constraints. Now the algorithms, the procedures that existed before were pretty brittle. And now you can just ask the LMs, when the LMs running the code, you can just say, can you find the inductive invariant 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 whereas before we had five humans who could drive these their improvers, those humans are now really excited because they're able to let the models go and do the proof search for like a agent tools go find the proof for them and they run thousands of these jobs at the same time. So we're getting like, it's not only like 10 X or 100 X or 1000 X productivity gains from that small seat of individuals who can drive these things. And the amazing thing is because these tools like lean their 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 or no.
So it seems like there's a couple of different or there's a spectrum of approaches where you could go buying like an LOM or reasoning model with these kind of formal methods where it's like, you know, verifying AI output or even something that stuff that you where the LOM 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 advertising. So I know you have to know that spectrum like what part of that I think it's like 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 is 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 them past and different institutions and I brought them to Amazon and basically the job is 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 actually don't see a ceiling for that productivity. The thing that I'm probably most interested in intellectually is agent safety to I think of agents as allowing us to see all things that were we only had sociotechnical mechanisms before. So now you have a choice of sociotechnical or these kind of agent tools and there's a disadvantage is advantages to them. Right. So 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. So like a 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 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. It's not AI is writing the code. You can't send the AI to jail. 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 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?
You know, CTL. What is the formalism for which you would want to express these things and then can use these auto formalization techniques to get them right. And then now can you in an agent execution environment before allowing the commands or programs that have been synthesized by the agents, LOM 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 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.
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 sort of unlocks a lot of a scaling dimension that's just previously unheard of. So the first problem is that if everybody's running, you know, a ton of different agents, like some points people are going to miss something because they're contest switching all the time. If you're doing this for engineering, you're spending out a ton of code. There's no way you can, you know, hand review every single line of code and make sure that'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, spat this out beforehand in terms around like what 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?
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. So the answer is yes. And there's a quote that's like this related to 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. 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 the decisions? I rely on the leadership principles to give me guidance. And in an agent setting where you don't have human judgment, you will want to be rather more concrete, but then you can use symbolic formulate 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 we 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 it's an exciting opportunity. I think it is the sort of scaling that you got glimpses of and really large success 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 scaling yourself, your family and organizations. 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 way. It's not just about the formalization of the spec, but also when the agent does something, be able to go back to the spec and actually check in a formal fashion, whether you're allowed to do that thing or not.
Is 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 aircraft. 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. 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 our answers 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? 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. Is this a good poem? I think that's a hard part is the things that are subjective. I've written a little bit about this where I think one of the reasons why we see success in engineering sort of really being the tip of the sphere 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 that you could if you generate code you could compile it. You run against tests. Those are some form of verification of whether there's correctness behind what you generated. But if I'm generating a poem or even, you know, I don't know a pressure lease about a product launch like the quality controls are much more subjective and it's hard to put some sort of formal verification around it to determine whether it's good or not. And then the back loop in engineering is also very fast where your you could you know, compile it past 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.
And then you can do that in the water 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 language that's not natural that's not English or something like the argument that would be made still ultimately in 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 me it's a mathematics or reasoning about correctness of programs or using 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 be to be to better problems fit into that class structure versus the just open ended kind of ask anything and get any possible answer. So I think that's a really good market for answering questions about correctness according to law and tax strategy across like a genetic financial systems is so big that it's worth going after. Even if we can answer questions around good poem. Yeah, healthcare probably some really interesting.
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. 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 we have a product called automated reasoning checks and better guardrails. It helps you formalize your domain like you know family medical leave actor 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 also allows you to understand your rules because there may be cases very rules were wrong and the customers like that can't be right. And so you can use the feedback from the customer store identify actually where you 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 LOM based situation. So on the other one around basically where like we regularly analyze using automated reasoning tools and entire 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 data flows to and from and then that allows us to make pretty high fidelity decisions around risk around information we're using to make decisions and so I think that's an area that the broader IT community can use to right if you're building a genetic 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.
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 want the agent to leak other customers. So one of the things that you said earlier was that there's only maybe two or three thousand people that kind of specialized 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, what is changed in particular for this to suddenly have sort of more visibility as an area that's important for building successful software. I'll give you this short term answer and there's actually a little bigger context. So I mean it's agent to get like 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 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 extra sort of art of the possible exercise. There were tools that use natural language that were very easy to call use one tool 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. 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. But before you were trying to talk about imagine a computer can tell you and they're like, I don't know what you're talking about.
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 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 larger change shows you how to prove a quickness of a program and von Neumann was a proof for all these all these people from the 1950s and 40s were mathematicians who knew how to do proofs and very clearly in their mind they understood the programs map to turn machine during machines or like automata. So 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 many computers and so on but the branches of the mathematical view of programs and how to reason about programs and then the IT industry kind of divided and so you meet people kind of didn't like you meet formal reasoning experts particularly in Europe who've never written a computer program their life. They don't have 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 practice programs so the world is 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 principle of mathematical right so automated reason 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 that makes them other those ideas and people are very excited and it was very heavy days but then you had this sort of series of AI winters or government funding would dry up for these areas that 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 can solve with their kinds of tools and were successful there and that's kind of where I grew up and then other people went to recognizing numbers for depositing checks and so there was another set of applications 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 and opportunity has really kind of brought all the communities the communities are coming back together and there are certain members of the crowds that are bilingual that can talk between all those communities and they're just worth their weight in gold.
Yeah, it's interesting. I think this whole area is bringing back a lot of things that have had periods of time where they were there was like a big research back and behind it. I think like ontologies certainly have been something that I did my PhD in the knowledge engineering space with ontologies and we're done on problems and then no one was talking about that. And now it's come back in a big way. There's a bunch of different things, 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 durable execution and durable functions and all this type of stuff that historically has been a little bit more niche certainly but it wasn't like everybody's problem and now suddenly everybody's problem.
And Amazon is funny because you know sometimes very big names will join Amazon and they'll hear about the automated reason and be like oh we tried that at my company 20 years ago didn't work. Well, maybe should be like maybe that was 20 years ago. So like things change and I think it's like music you you see ideas like old ideas in our 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 actually frankly good because I think it's good to get a mixture of ideas and people confused about them and some people are all getting for some and some people are getting further and then finding combinations and that it gives diversity of thought which I think is a lot of things that are going to be more. So it gives diversity of thought which actually helps us solve problems in better ways. So that's pretty exciting actually.
Yeah absolutely. 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 working in that area kind of like walked into a certain way. Yeah, totally. 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. I would have you like give me another year give me another year. Yeah absolutely would have never solved it where I would have just hit camera in that nail and eventually we 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 what tools you know books practices would you 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.
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 Java and Rust and so on but it unifies to the logical representation which ultimately this is something called lean. So lean there's a thing called lean there's many other things. So Isabelle whole light lean so on but lean is the one that many mathematicians have sort of clicked to so that's the becomes the lingua Franco for them and because of language model training so language model providers discovered this data begin training over and saw the value of the state so then they've now begun to synthesize data using leans for example deep seek to that reinforcement learning together with lean is 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 mathematicians tool and it requires you to traditionally to hold its hand it's not it's automated reasoning is sort of almost a misnomer right it's like very far from automated I mean it's not a little bit more like very far from automated I mean it automates the checking of the argument you found right whereas these tools like a positional satisfiability solver like catacol is fully fully automated but it's only 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 opened sourced and then to reason and lean and then one could imagine you know products are coming up with the data.
So products are coming up there's startups in the AWS we're all kind of building products in this space so there will be various products and you know love for people these AWS ones but there's other startups that are building stuff too so. Yeah 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 actually have a way to get access to information that you never had access to it reminds me of like you know when I was a teenager in the internet became something suddenly do not have to go to a library look up the information you have to look at 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 the time and I think we're so excited about it. Totally yeah when I look at like you know I used to work on Volkswagen motors like Aircool in 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 or 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. 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 trying to post just a few things but they should be kind of interested people who are tracking formal methods on Byron Cook. Yeah I don't know probably not I'm just kidding keep doing it.
Alright 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 was a pleasure thanks for your time.