伟大的安全更新：AI ∧ 形式化方法——RAND的Kathleen Fisher与AWS的Byron Cook

Today, we're diving into the world of automated reasoning and formal verification of software. My guests, Kathleen Fisher and Byron Cook, are legends in this underappreciated but increasingly important field. Kathleen famously led the High-Assurance Cyber Military Systems, or HACMS, project at DARPA, is currently the director of the Cybersecurity Initiative at RAND, and, starting in February, will take over as CEO of the UK's Advanced Research and Invention Agency, ARIA. ARIA is often described as the UK's DARPA, though its mission goes beyond military technology, with the goal of unlocking scientific and technological breakthroughs that benefit everyone.

Byron, meanwhile, is vice president and distinguished scientist at Amazon, where he's made a major contribution to cloud security by leading the application of formal methods to distributed systems at AWS. Despite being arguably the world's biggest target for cyberattackers, AWS has maintained an amazingly strong security record.

In all honesty, I don't think I've ever felt more outclassed by my guests than I did in this conversation. My own math career topped out at differential equations and complex analysis in college, and I've never been strong when it comes to mathematical proofs or formal logic. Nevertheless, I'm hearing more and more in AI circles, not just about the need to harden critical infrastructure against cyberattacks before AI-powered hacking becomes ubiquitous, but specifically about the unique power of formal methods to deliver true information-security guarantees.

And so, I was really eager to learn as much as I could, and honored that these masters were willing to answer my remedial questions. We cover a lot of ground in this conversation, from the nature of the cybersecurity threats that AI poses to the relationship between software specifications and the proofs generated by formal methods, the critical role of assumptions, and how we can be confident that many low-level logical statements do, in fact, add up to system-level guarantees.

We also discuss how these methods can be used to create a reward signal for coding models, and why, despite what we've seen from AI coding assistants to date, we should expect LLMs over the next generation or two to achieve superhuman levels of code security. That could create the opportunity for a great society-wide software rewrite that could dramatically and durably reduce cybersecurity risks.

Finally, we explore how AWS is applying these methods to AI agents in the form of its new Automated Reasoning Checks product. In short, by translating natural-language policies, like a company's HR handbook or a city's zoning laws, into a set of variables and rules that a user can iteratively run test cases against and refine, and then mapping an AI agent's output onto this structure, the service makes it possible to use formal methods to check an AI agent's work for policy compliance.

The translation from natural language to formal rules does create some gray area that isn't present in the traditional process of formally verifying explicitly coded software, but this approach nevertheless stands out to me as one of the strongest I've ever seen for implementing AI agent guardrails. So much so, in fact, that toward the end, for the first time ever, I found myself worrying that AIs might one day become so consistent in their adherence to policy that we could lose the flexibility to make exceptions when official policy doesn't fit a particular situation. That, ultimately, is a problem for another day.

For now, the bottom line is that, with threats ramping up everywhere, the techniques we discussed today constitute one of very few strategies I'm aware of that could really work, in the sense that they're capable of resolving specific, critical vulnerabilities once and for all. This is challenging material. If you're like me and you find that some of this conversation is over your head, I would encourage you to pause and chat with your favorite frontier language model to clarify key concepts. I'm confident that if you do, your AI worldview will be stronger for it.

I hope you enjoy this technically demanding but deeply optimistic conversation about the future of AI and secure systems with Kathleen Fisher and Byron Cook. Kathleen Fisher, director of the Cybersecurity Initiative at RAND and soon to be CEO of the UK's ARIA, and Byron Cook, Amazon vice president and distinguished scientist, welcome.

Thank you.

Yeah, glad to be here.

I'm really excited about this conversation. The world of AI and its impact on cybersecurity is obviously heating up at a tremendous pace, and a lot of people are worried about what this is going to do to the offense-defense balance when it comes to securing our digital systems. You two are both world-leading experts on this topic, and I'm really excited to develop my intuition and help other people develop theirs about where we are, what threats we have, and what threats are emerging as a result of AI.

Then there are these, I would say, formerly little-known—or you might even say esoteric—but increasingly central methods that you guys have pioneered: formal methods that can hopefully give us a qualitatively different level of confidence in the systems we're building and how much we can rely on them, and ultimately create that sort of DEAC future that we can all live safely and happily in.

So teach me everything, but let's start with how you see the impact AI is having right now on the cyber landscape. Is it already happening? We hear it's coming, and Anthropic has put out a report, but I don't really know how to think about it.

One way would be that chatbots help people who aren't that capable become more capable, but maybe they're just attacking people who otherwise had security by obscurity, and it's not really that big of a deal. Maybe we're going to see these AIs coming up with cybersecurity move 37 type, brand-new zero-day exploits, and it's going to be crazy.

Maybe the way to think about it is that hackers have historically been limited by the fact that they can't share or collaborate in very broad networks, so they're only able to attack a few things at once. Maybe AIs could make that a super-parallelizable sort of thing. What do you think is real and what is fake when it comes to AIs changing the threat landscape in the cyber domain?

I think, sadly, it's all of the above. AI is providing assistance at all levels of the cyber kill chain and at all levels of expertise. It's making people who don't know very much know more, people who know some know more, and experts more effective. It's making hackers able to work at scale and in parallel.

I have colleagues who are really powerful reverse engineers, among the best on the planet, and they are shocked at how good AI tools are at helping them do their jobs better, or how well those tools are able to do on their own. So everything from script kiddies to nation-state adversaries: AI helps everyone do better at cyberattacks, or whatever part of the cyber kill chain you're functioning in. AI helps you do better at that skill.

I agree with Kathleen, but I can give a slightly more optimistic take on it. It also helps the defender. One of the things we've depended on for a long time is the absence of mechanisms. We humans wrote code, and then we didn't really know what the programs were doing, and we hired some good people to try and figure out how they were written.

But as we're using these agentic AI tools, there's a movement away from sociotechnical mechanisms toward formalization. I think there is now a feedback cycle: as security events happen, we can say, "Oh, we don't want to ever be in that situation again, and here's the property we could write down and then show is true of the code." So I think each incident has a tremendously greater blast radius for improving the systems of the future. But I'm speaking to the future; I'm not just speaking to this moment.

Yeah, I think that, to answer your question, right now the software we have is riddled with vulnerabilities, and AI will make it easier to exploit those vulnerabilities for all different kinds of attackers, from script kiddies to ransomware gangs to nation-state attackers. It can do that either in a subtle way or in an overt way, or cause an AI agent to run amok. All of those threats are made more intense by AI.

I think that's the doom-and-gloom scenario. The same technology that is producing that doom-and-gloom scenario, though, can be flipped on its head to make the software less vulnerable.

We're talking about software, of course. We have hardware, software, and people, right? All of those things are potentially affected by AI systems. Formal methods paired with AI can potentially help with many aspects of the system, not just the software, although I think software is the sweet spot where we have the most ability to make a positive difference relatively quickly.

For somebody who, like me not very long ago, had either not heard of formal methods at all or had heard of them and had a very primitive understanding, can we do a little 101? What are formal methods? What is the formal verification of software? What does it allow us to do that's qualitatively different?

It's the algorithmic search for proofs. What is a proof? It's a finite argument of what is true. You can reason about the infinite in finite time and finite space.

To do that, you need chess-like rules. You need an accepted set of a small number of rules that, to make an argument, you have to religiously follow. Those rules have evolved over the past 2,000 years, but we have, as a society, settled on a few of them, like modus ponens and so on.

Basically, you follow these rules, and these days we can algorithmically search for those arguments. Generative AI is actually very good at helping us with that. You can use generative AI to help find a proof and then check it according to one of these checkers that only follows those rules.

I would say, at a slightly higher level, it's a set of mathematical techniques that let us prove properties of software in a way that we can check—the machine can check—so that we can make sure that we did all of our work properly. That allows us to prove properties of software.

Those properties aren't a one-size-fits-all thing. There's a whole range of different kinds of formal-methods-based properties. The gamut goes from things that are really easy to use and easy to understand to harder-to-use methods where you prove richer properties.

A type system, like the type system in Java, is actually an example of a formal-methods-based property. When you run the type checker in Java, it proves that the way your program is manipulating data means you're only ever going to put integers together in a way that is consistent with integer-like behavior. You're not going to try to add an integer and a function, for example. That would be a type error.

If you've ever written a Java program and run the compiler, you've used a formal-methods-based property. The type checker has checked your work and given you the seal of approval. You've used that formal-methods-based approach correctly. You didn't have to know very much about how it was doing it. You just had to know the rules for how various kinds of types could interact appropriately, and the compiler checked that those rules were used properly.

There's the escape hatch of a type cast, which you have to avoid if you don't want to break the soundness of the type system. That's at one end of the spectrum, where it's actually pretty easy to use and you get a relatively weak guarantee. Type safety is a pretty weak guarantee.

At the other end of the spectrum is an interactive theorem prover, where you're proving full functional correctness. You have a specification of exactly what the code is supposed to do. CompCert is a verified C compiler that proves that the C code maps down to assembly code with exactly the same semantics. That was proven in an interactive theorem prover, where the people doing the proof had to use a huge amount of brainpower to prove that it was correct. Each step of the logic was checked using modus ponens, like Byron referred to.

That's the other end of the spectrum, where you're talking about PhD-level smarts to use. There's a whole bunch of things in the middle, where you have an intermediate level of property and an intermediate level of how much elbow grease you had to use to get that property proven.

All of them are useful. Everything from very simple properties like type safety to very high-end properties like full functional correctness is useful. It's just a question of when we want to use this level of effort to establish what kind of guarantee. Choosing which properties and what level of effort for what kind of thing is part of the art of appropriately using formal methods. Did that make sense?

Yes, although I definitely have some follow-ups.

Please.

My software background is basically more on the JavaScript side. I haven't even gotten very far into TypeScript, so I've written code where I can add an integer and a string. If I do that, it's on me.

I then do what I think most rank-and-file web developers, including many building on AWS, are doing: throw some code together, fire the app up in a browser, click around, and see if it's doing what I want it to do. If it's generally doing what I want it to do, then I feel like, okay, I guess I did a good job.

Obviously, in that process I'm not able to be anywhere close to exhaustive in terms of all the possible things that could logically go wrong. I definitely have an intuition for how type checkers, for example, can help reduce errors, because things that I wouldn't have thought of, these tools can flag: “Hey, you're breaking a rule here, and if you do that, you could get yourself into trouble.” That much I think I have a decent intuition for.

When you use something like JavaScript, you're getting memory safety, which is another kind of formal-methods guarantee, right? The memory boxes have an abstraction that the language is providing for you. When you store something in memory—when you store an integer in memory—when you take it back out again, it's still an integer. It didn't transmogrify itself into a function. That's a memory-safety property being provided by the language that you're using.

If you're using C, that's a language that doesn't provide memory safety. Memory safety is another property that is very useful for not getting hacked. It's a property that the language you're programming in is providing, and the interpreter that you're using is enforcing that particular property.

Help me understand this basic idea that these type checkers can help me avoid shooting myself in the foot. I don't even have that great a sense of the taxonomy of attacks. Memory attacks or type attacks could be one. In my homework for this, I've noticed that parsers are maybe not the root of all evil, but a very common sort of weakness. Memory safety, type safety, input safety—yes.

So maybe give us a little walkthrough of the kinds of things that people tend to exploit and then the kinds of approaches that people take. This is where I get so fuzzy, because I'm like, how do I really know when it was fully correct?

How do we get to that level of confidence? The layperson who doesn't quite get it can wonder, “What if there was a mistake in that process? How do I know that it's truly proven in a way that I can accept it and take to the bank?” That's a fuzzy question, but I'd love to work my way toward having the confidence that I believe is well justified. I can't articulate yet why I can sleep soundly at night because this process has been executed.

To some extent, cybersecurity is analogous to the security that you would want on your house. One hundred percent security is not actually a goal that you should really be going for. You don't want to have a house that no one can ever break into, because then if you lost your house keys, you would have to go buy a new house.

You want a house that has an appropriate level of security. Right now, the level of security we have is equivalent to the doors being open. The windows are open. They're not even closed, let alone locked. The question that you're asking is a little bit like—yes, we can walk through the example that you're asking for, but total security is way, way, way beyond where we are. We're looking for the equivalent of closing the doors and locking them, as opposed to everything being wide open, which is kind of where we are right now.

Yeah, the mental model I have is that there are a set of properties that you want to hold of your systems. They can be motivated by security concerns, past things you've seen, and also where things are going.

You might want to know that no credentials are ever logged and that all data at rest is encrypted. You can layer on more and more of these. Maybe for sovereignty, you want to know that certain data never leave the region.

To establish some of those things, you'll probably need to establish—you might need to establish—memory safety. You might need to establish various things, but maybe you don't, right? The way I like to think of it is: What properties do we want to hold? That creates an envelope in which the system can operate safely.

And then the programmer or the LLM can choose to implement that in different ways. So, I think that notion of totally proving everything about the system isn’t really true. I think that you want to underspecify the system and then allow there to be different implementations of that program.

The other point I’ll make is that you’re always having to make some assumptions. When you prove a program correct, you typically assume the microprocessor is correct. We could go prove that, but ultimately, if we prove the correctness of the microprocessor, we’re going to be making assumptions about the principles of physics. We don’t really know that they’re always going to hold. We believe historically gravity has held, and we believe it’ll continue to hold, but we don’t really know that. You’re not going to be able to do a mathematical proof of that per se, and if you do, it’s going to be under more assumptions. So, there are always assumptions all the way down. You’re only ever raising assurance; you’re never getting 100% assurance. But it becomes confident enough—

Yeah, exactly.

—that you have assumptions that all the air in the room isn’t suddenly going to move into the corner, and that’s good enough. Even though theoretically it’s possible that all the air in the room will move into the corner and you will suffocate. It’s that kind of thing.

I think there are properties like, if your system is memory-safe, if your system uses parser generators and is input-valid, things like that will make it so that the likelihood that your system is vulnerable to certain kinds of attacks is much, much lower. Those things are the equivalent of having the practice of closing and locking your front door, and closing and locking your windows. It doesn’t mean your system isn’t vulnerable; it just means your system is likely to be much less vulnerable, and the people who are attacking may attack their neighbors instead of you.

So, what we’ve done at Amazon is listen to customers about the concerns that they have, and then choose to focus on proofs of some of those things. The other thing we’ve done is work with engineers who are developing systems and identify the parts that we’re worried about, or that seem hard to get right. Then we focus there.

We’ve identified pieces of the system and done proofs of them, and what we’re seeing over time is that they’re beginning to spread and start to touch. You’ll have proofs of 2 systems, but those proofs begin to touch each other, and they begin to blur into the system, parts of which have been proved.

The big thing is: what are customers worried about, both internally and in terms of policies, networks, and that kind of thing?

I’d love to go through some examples of customer concerns and the types of assurances that you’re able to give customers based on all this work. But maybe, before doing that, just one more beat on the C compiler.

When you said that it’s proven to the point where the semantics of the C code are proven to be reflected in the semantics of the machine code that it’s compiled into, what assumptions are still lurking there? I have an intuitive sense of what it means to say that the semantics are the same, but I’m unclear on what assumptions that would rest on. What’s the equivalent of the air all going into the corner for that scenario?

I don’t remember off the top of my head what the assumptions were. They’re probably assumptions about the underlying hardware. For sure, they’re going to assume the correctness of the ISA. I only know the work secondhand, but they didn’t go prove the x86 or ARM instruction set. They’re assuming the x86 or ARM instruction set, and they have a hardware model of what that is. That’s what we do in our work at Amazon, too.

The original version had assumptions about the parser that turned out not to be correct, but they went and fixed that in a later version. They’ll also probably make some assumptions about the code. I don’t know what they do for concurrency, if they do anything, so it’s probably sequential. The original version was sequential because they were focused on avionics software. Avionics software is assumed to be single-threaded. So, there’ll be some assumptions along those lines.

When you’re calling the operating system, there’ll be some issues around that. There’ll be assumptions about what the operating system’s APIs do, and there will be other third-party APIs that they’ll have to model. The nice thing in this work is that you can model the outside world, and you can often model it with demonic nondeterminism. You can say, “I don’t know what this thing is going to return,” and a formula represents that uncertainty.

Nondeterminism isn’t free, but it’s already paid for in the formal reasoning tool, so it’s actually quite nice. Then you can refine that as needed. One of the areas of practical reality when you’re doing these kinds of proofs is that you end up refining your assumptions around third-party APIs, like operating-system system calls.

Can you give me a little more flavor of how these proofs work? It might be useful to do this with examples, starting from customer concerns—or maybe not; you tell me.

What do these proofs look like? I have the sense that they’re exhaustive mappings out of every possible logical state, every possible corner case. I’ve heard estimates that the length of the proof might be an order of magnitude longer than the code that you’re trying to prove the validity of, maybe even longer than that. If we started to inspect the proofs, what do they look like?

There’s a huge diversity of tools, and they make a number of different choices. It’s like looking at all 80s bands and then trying to characterize what a pop song is, right? Some of them are really heavy, some are super simple, some are long, and some are short.

Kathleen was alluding to this: there’s a spectrum of tools, and some are really easy, while some are really hard to use. With generative AI, maybe they’ll be easier in the future. There are also tools tailored to certain domains.

For example, there’s a technique called predicate abstraction and counterexample-guided abstraction refinement, which is good at proving certain kinds of properties, such as API usage properties.

They run completely automatically on the code. You don't need to do anything. They discover a proof, and then, if you want to investigate it, it has a particular shape and sort of representation.

But then, if you're trying to prove the—I don't know—the Collatz conjecture, or if you're trying to do something more complicated, that's a different story. At Amazon, we've recently announced the proof of a new hypervisor. We've announced the existence of a new hypervisor called the Isolation Engine. It'll be in the AWS stack, Graviton 5, and we have an Isabelle 3 proof of it. We've proved a bunch of properties of that, and those are quite intricate.

So there's really a spectrum. I could give you, for any data point you want, an example. Let's do a couple of relatively simple ones. For proving the correctness of the TLS handshake in AWS to it, it's an open-source implementation of TLS that we wrote at Amazon, and it's what Amazon uses all across Amazon. It's all completely automatic.

Underneath the hood, the tool being used is sat with the discovery of inductive invariants. Cryptographic code usually has fairly simple loops. The loops aren't over complex data structures, and so on, so fairly simple heuristics actually work.

That's one example that's quite easy, whereas in the proof of the hypervisor, my mental model is that there's sort of a 1-to-1 ratio of engineer to formal methods expert on the team. I imagine—I haven't looked at it in great detail—but it's on the order of that size. It's going to be roughly a 1-to-1 ratio of proof scaffolding to code. Those are a couple of examples.

Can we go a little bit further into what sorts of statements are being made? “This software does what it's supposed to do and only what it's supposed to do” is a great place to get to, but I still want a little bit better intuition for how all these low-level statements that we can make aggregate up to that, and how we know that they do.

I apologize if this is a really ignorant line of questioning, but I do struggle with this. I can look at these individual statements and say, “Okay, we've gone down this logic path, and that one's okay.” We could do that a lot of times, and I'm still thinking, “How do I know that we're actually proving the things that we mean to be proving?”

I think it depends on the system. SEO4 is a separation kernel. It's one of the exquisite artifacts that was proven to be fully functionally correct by a team in Australia. The main property of a separation kernel is that you can configure it so that you have different compartments, and the code in one compartment cannot interfere with what's happening in another compartment. They specified that property in formal mathematics.

That was a massive undertaking. There's about 10,000 lines of C code that make up the hypervisor, and then about 100,000 lines of Isabelle proving that the property holds and that you have integrity of the system. The reason why that level of effort was worth it was because that is a building block that you can use in many systems.

In HACMS, which was a program that DARPA ran from 2011 to 2016, one of the things the HACMS performers did was build a helicopter, the Boeing Unmanned Little Bird. They used the SEO4 hypervisor to separate the code on the helicopter into different partitions. One of the partitions was the camera partition, which an analysis suggested was not important from a security perspective. It didn't matter if the camera partition was owned by the bad guy for the flight operations of the helicopter, or for the ability of the helicopter to communicate with the ground station.

Then there were the flight operations: the thing that controlled the actual ability of the helicopter to fly. The mission control computer was the thing that talked to the ground station, and there was the flight computer, which actually controlled the ability of the helicopter to fly. They analyzed the system and modeled the overall architecture in another formal language called AADL, the AADL architecture description language.

They wrote the protocol for communicating with the ground station in a grammar instead of writing it by hand. They wrote the grammar for what the message format had to be, and they proved system-wide properties. The only way to communicate from the ground station to the helicopter was through a pathway that had to be authenticated and encrypted. All messages that got from the ground to the mission control computer had to be authenticated and encrypted—properties like that, which are the high-level system properties that you cared about.

They reasoned about those properties in this architecture-wide description, which is a formal methods tool. Using that combination of formal methods tools—things like the parser tool, where they wrote the description of the properties; a cryptographic tool, where they wrote the formal encryption tools and proved properties of encryption; and then the SEO4 microkernel, which is how they got the separation property—they were able to prove system-wide properties like the fact that the only way to get a message to the mission control computer was through an authenticated, encrypted channel. They were able to prove those kinds of system-wide properties that you were asking about.

They then tested this with a red team. They let the red team put whatever code they wanted in that camera partition, which they had analyzed at the system-wide level to decide wasn't critical to the security of the overall system. At the end of phase 2, they let the red team attack the system while it was on the ground. At the end of phase 3, they let the red team attack and try to disrupt the operation of the helicopter while it was in flight, with 2 test pilots on board.

They were basically trying to crash not only their partition but the helicopter while it was in flight with test pilots on board. The test pilots not only survived; they couldn't tell that they were flying the high-assurance version of the helicopter instead of the normal version. The camera partition kept crashing because the red team could crash its own partition. They could basically do a fork bomb, and that would bring down their own partition, but the rest of the system would be like, “Oh, the camera partition went down. Let's restart that partition.”

So that's an example of how you can use a combination of different formal-methods-based tools to get system-wide guarantees of behavior, right?

Yeah. One question I still have there—and that's an awesome story—is that you kind of glossed over the beginning part of the story. As I understand it, before this whole project began, the red team hacked right in and surprised the Boeing engineer. The baseline of hacking was that this was a military helicopter, right?

They also did the same thing with a quadcopter, and no one was surprised that the red team could hack into the quadcopter. The Boeing engineers were quite surprised that they could hack into Boeing's helicopter. DARPA had the red team attack the platforms unmodified to demonstrate what the baseline security was, basically to show that these platforms were hackable without that much effort. The red teams were able to hack in with about 6 weeks' worth of knowledge in the first place.

After the modifications, the red team was following along throughout the whole program. One concern people have voiced is, “The red team didn't know very much about the system, so why would you think they would be able to hack in?” The answer was that the red team actually knew a ton about the system because they were following along through the program the entire time.

On the quadcopter, DARPA took it back to DEF CON and to the Aerospace Village and had hackers try to break into the quadcopter several years later. No one was able to hack into it several years later, kind of demonstrating that these kinds of techniques really pass the test of time. There are still assumptions, so it probably is possible to hack into it, but probably you have to attack through the hardware instead of through the software.

Yeah. My one main remaining question on that story is that, at the end of that process, for somebody like me who maybe doesn't get it, there's no substitute for flying the helicopter, right? But how much lingering doubt did you and the team have about whether the red team was going to get in?

When you say something is proven, in your mind is that 100% proven, or is it, “How many nines of proven is proven?” Was it purely for the doubters, or the people who don't get it, that you needed to do the flight? For your own sense of epistemic certainty, did you have everything you needed before the bird even went up?

Yeah. The flight was, I think, mostly for the demonstration quality. The people writing the program were willing to risk the lives of the pilots, but I think everyone in the program knew that it was going to be fine because of the level of guarantee it had.

It wasn't just the proof; it was all of the surrounding reasoning and artifacts that went into producing the evidence that was in that proof.

I mean, it’s probably still hackable. There are still, as Byron says, always assumptions. There’s always more to prove. There’s always more to prove, right?

But what the attackers could do in that case—given where the red team was and what it was going to be able to do—was not going to be enough to crash the helicopter in that situation. Could somebody come and attack it in a different way? Probably. Could somebody throw a rock at the rotors of the helicopter and crash it? There are other ways of attacking the helicopter that would cause a problem. Helicopters are fundamentally not very stable, right? So, is the risk to the helicopter through another means now higher than the risk of the software attack? Probably.

If I could propose a way of thinking about it, we could separate the how and the what. I imagine there’s—I mean, the problem is undecidable, so this won’t be possible—but imagine there’s just this magical tool that can answer any question and find any proof. Now, there’s still an infinite set of questions you could ask of that tool.

So it’s like a query tool, right? Imagine Google Search: you type a question and get an answer. So imagine we have a procedure that can answer questions about your program. You have a program and a tool that can answer any question about it with 100% reliability. There’s an infinite, if not uncountable, number of questions you could ask.

And so imagine you knew all the answers to the questions you had asked. You had 5,000 questions; there might be a 5,001st question you want to ask that might reveal something you actually didn’t like about your system. That’s one way to think about it. What’s traditionally been a problem, and what can make this area difficult, is that actually establishing the answers to those questions is also rather challenging.

There are quite remarkable steps of progress happening now to make that easier, and that sort of brought it to the forefront. But the other thing that’s brought it to the forefront is that with generative AI and agentic AI, suddenly a much larger set of people are asking those kinds of questions. So it becomes much more interesting now.

So, yeah, tell me where we are today. I mean, you’ve been working on this at Amazon for a decade, right? And there have been a lot of wins. Maybe sketch out some of the big wins. What are they? For a little developer like me, I just trust you guys are doing a good job. I don’t think too much about the how. I know big enterprise customers that are making decisions to move highly sensitive data into AWS are asking a lot harder questions than I’m asking. So, how much of the roadmap has been accomplished? How much remains to be done, and what does the acceleration look like today with the augmentation that we’re getting from generative AI tools?

Yeah, let’s say that, before 2022, the things that we had done were, first of all, building tools to help customers reason about their configurations—their virtual networks and their policies. In AWS, as in many cloud compute environments, there’s a notion of policy that’s quite flexible. Basically, you have resources on the internet, and then you have policies that define when those resources can be accessed and the constraints under which that can happen. So a secure system is typically a configuration of those policies, which turns out to matter quite a bit.

When I joined in 2014, customers loved the flexibility of the policy language and the flexibility of the virtualized networking environment, but they didn’t love not knowing whether or not they got it right. One of the first things we did for customers was build tools to help them actually reason about their own systems. Those are embodied in many AWS features, but the flagships would be IAM Access Analyzer and VPC Reachability Analyzer, to reason about the policies and the networks.

We also have S3 Block Public Access, and there are also tools in Amazon Inspector and AWS Config Rules in a bunch of places. Internally, we identified a bunch of places where we wanted to get things right: the cryptography, the virtualization infrastructure, the storage infrastructure for durability, and the identity infrastructure. We have proved a number of key lemmas in that space.

What’s been very interesting lately is that we proved the “correctness”—and I don’t think the audience will be able to see me, but they’ll hear me, so there are quotes around “correctness”—of the policy interpreter. The AWS policy interpreter gets called more than 1 billion times per second. Whenever you call an AWS API, we gather all of the policies related to the principal and the resource, put them together in a collection, and then call this interpreter to make a decision: yes or no, should we allow this action to take place?

Now, what does correctness mean? It’s correctness with regard to the semantics of the policy language that we defined in that previous tool, which is the basis of IAM Access Analyzer. That’s an example of these tools beginning to connect up. We first defined the semantics of the policy language, then provided customers with tools to formally reason about their policies, and then customers began to ask questions like, “How do I know that you’re actually interpreting that policy correctly?” Well, okay, let’s go prove that. You see that in other places in the virtualization space and so on.

Then, very interestingly, what happened in late 2022 and early 2023 was that, for obvious reasons, suddenly people became very interested in generative AI. Coming back from the holiday break of 2022 to 2023, boards and C-suite leaders really wanted to develop stories for what their organizational generative AI story was going to be. A whole bunch of people began using generative AI tools.

The questions we began getting from customers evolved, and it became much more about, first, the correctness of chatbot applications and then, increasingly, the correctness of agentic AI and multi-agent systems. Under the hood, we’ve been applying many of the same techniques to agentic AI and chatbots. A policy of the Family and Medical Leave Act is very similar to an AWS policy on S3 buckets or VPC networks. Reasoning about the composition of multi-agent systems actually looks a lot like reasoning about the composition of microservices to show that S3 provides strong consistency as opposed to eventual consistency.

We’re able to take a bunch of those techniques and adapt them into that world. That’s where we’re at. The other area that’s quite exciting is that generative AI can actually help you find proofs. When you’re asking your generative AI tool to help you find a program, you can ask it to find a proof at the same time.

And so you can begin to check those proofs as the programs are synthesized. The big challenge has always been, and I imagine Kathleen will agree with me, figuring out what you want to prove. A lot of the work that's been going on recently—you'll see this in Automated Reasoning Checks and Bedrock Guardrails from AWS, but also Kyber, which is an IDE that Amazon has launched—is helping customers figure out what their specification is: What do you want to hold of the system? Let's iterate together on that to make sure you got it right, so you're actually proving what you think you're proving. That's where a lot of focus has been right now. So that's kind of a snapshot of where we're at.

It might actually be helpful to dig in a little bit on the Automated Reasoning Checks as they relate to the LLM and agentic system outputs. I think this feed is by an AI obsessive for AI obsessives, but as much as I'm obsessed with all the latest developments in AI, I'm also not very good even with my own password-management-level security. So I think maybe the intuition will be a little bit easier to develop for the more familiar use case, and then we can backport a little bit of that intuition to the rest of the world.

One of the promises that the Automated Reasoning Checks make is that you can minimize AI hallucinations and deliver up to 99% verification accuracy. It might be helpful to talk through how this sort of policy works, because what people can start with, I think this is really interesting, is a natural-language policy. You mentioned the Family and Medical Leave Act policy. This is something that somebody has written in prose, presumably without even thinking about a software implementation when they wrote it, right? These policies typically predate the ChatGPT moment.

Then somebody comes along and says, “Okay, I could really save a lot of time and money if I had an AI evaluate everybody's FMLA applications.” But then we have the question of whether it's doing it right. So maybe take us through that loop of how this fuzzy, natural-language policy gets translated into a set of checks in the first place. There's also an iterative loop, which is part and parcel of everything I've seen in the AI game recently. Take us through that story of how a policy becomes a formally, or almost proven, policy. It's like how a bill becomes a law, but it's how a policy becomes a formally or almost proven policy.

You can go today and ask Claude, “Hey, translate this. Here's this PDF. Can you please translate it into temporal logic—branching-time or linear-time temporal logic—or SMT or Lean? And then I want to answer these kinds of questions.” Under the hood, that's essentially what the product is doing.

There are 2 activities in the product. The 1st is to help you formalize what is true, and the 2nd is to remove incorrectness due to hallucination at inference time. We basically ask a generative AI tool to help translate it. Now you have the problem of, “Hold on. We just used generative AI to formalize this, but I thought the whole point was to address incorrectness due to hallucination in generative AI.”

What we can do now is walk through the structure of that formula, identify interesting corner cases, and walk you through what that formula is really giving you. You have a non-expert who probably doesn't understand logic, but we can calculate all of the representative corner cases and walk you through what answers you're going to get. If you don't like what you're going to get, then you can refine it. You can say, “I don't like this answer. Here's why,” in natural language, and we can go back to the generative AI tool and do that again.

That kind of models what we've been doing all along at Amazon and throughout my entire career, and I imagine Kathleen will agree. Traditionally, you would have paired up a formal methods person with a domain expert in the other domain—biology, operating systems, device drivers, airspace, railway switching, you name it. Together, you're going to build a formalization and look at a bunch of examples. The domain expert is going to say, “Oh, no, you got it wrong. You didn't understand the assumptions.” You bake those in, do it again, and iterate until you can't find any more problems. Then you say, “Well, I hope that's what we're trying to prove,” and you go prove that against the real code.

That's kind of what's happening in the system, too. There's a neat feedback cycle after deployment, which we'll talk about in a moment. So now let's talk about deployment. Once you've locked that in, you can deploy it. If your customers or users of your chatbot are asking questions, we translate those into natural language, and then we prove or disprove the correctness according to the formal model.

There are a couple of other gotchas. How do we handle the natural language? Again, we use generative AI, but now we don't want to do this loop. What we do is multiple translations, and then we use a theorem prover to see whether each of the translations is equal to the others. If so, our assurance that we got the translation right is relatively high. That's why we're at 99%, not 100%.

If not, then we can do a form of active listening. If one translation said, “They're talking about a first-class flight,” and another translation said, “They're talking about a coach flight,” then we can go back to the user and say, “Did you mean first class or coach?” Or we can query that in a database. There are various methods there. There's a sort of active listening to build a mental model about what the question is, and then we can prove or disprove that according to the model.

That's the kind of product. By the way, this is for corporate policies and these kinds of things, but you see very similar things happening in code, and you see very similar things happening in agentic systems. You see this pattern of the human in the loop translating data to knowledge quite a bit. Deployment into the inference system, either over natural language or structured systems like programs, is the downstream place where that gets deployed.

Let me try to echo a little bit of that back to you. I think that was really good. In the traditional setting, you said—and it's essentially the same for the generative AI setting now—you start off with a fuzzy idea of what it is you want to be doing. You have to bring in the domain expert who has, if nothing else, the ability to answer the question, “Are we doing the right thing in this case?” You're trusting that person's judgment to be ground truth for what you want to happen.

Hopefully they've been able to capture that in written language, but probably not 100%. They get together with a formal methods person and translate natural language into a logical specification. They then run a bunch of examples through and validate that this all seems right, at least so far. In the traditional sense, this would probably be the biggest weakness, right? Did you get the specification correct?

Yes, by far. It's the hardest part. Even though, once you have a specification and you're reasoning about programs, the problem is undecidable or intractable—NP-complete—by far the hardest part is the 2nd thing. In my career, working in large organizations, I've spent a lot of time on shuttle buses between buildings trying to get agreement among teams on whether we got the specification right. I've spent a lot of time doing that kind of thing.

[laughter]

Okay, so that's interesting, and that obviously becomes one of the assumptions on some level: We're only as good as the specification.

I'll give you a concrete example that's pretty illustrative.

Please do.

For various compliance reasons, like SOC 2, and various compliance regimes around the world, there's going to be one around “all data at rest is encrypted.”

Okay, sounds plausible.

But then, what do you mean by encryption? Exactly. If I use an encryptor that I get from a cereal box, that's encryption. Well, no, that's not encryption. That's the issue: How do you define encryption? Uh-oh. Now we're talking about what you mean by encryption, and so we're iterating on that.

Then we could talk about what “rest” is. What is “rest”? If I put it on the table, is that at rest? Oh, no. You mean digital storage. Okay, so now what you mean is digital storage, and then you can talk about what happens if the data is flying in a network and you're using the latency of the network such that it never actually gets stored to a disk drive, but is just going around and around the world. Is that at rest or not?

Because if that is at rest, then it probably doesn't hold, because that's not what we're proving, right? So you do have to define that “at rest” means these media or these APIs, and “encryption” means data coming out of these APIs. You have to get real clear on what those are.

And so, that has already gone through 3 or 4 refinements, and that’s just for a very simple case.

Yeah, that’s fascinating. So, in the traditional, pre-GenAI context, you have your spec. You go do a bunch of work that’s above my pay grade to prove that the software as written satisfies the spec.

Which it won’t.

So, then you have to fix it.

It won’t.

Yeah.

Yeah, it won’t. Exactly. And then you’re going to have to—

Oh, yeah, that’s the other thing: people have cognitive biases around, “No, that’s not possible.” Right? So, invariably, when you’re doing this process—when you find what you believe to be a bug, you get 3 engineers from the team together, put it up on the board or whatever, and show them the bug. One of them will say it’s a bug, and 2 of them will say it’s not. And now you’re going to need a—

Some people are going to be pessimists, and some people are going to be optimists. They’re like, “Oh, that’s not possible. The environment will never—”

Be the conditions, right? The environment will make it so that could never happen.

Yeah, that can’t happen. And then they’ll argue amongst themselves. Really, the only way to get to ground is to create an exploit.

Yeah.

To show that it’s possible. To show them that it does happen. You identify those exploits by finding places where the proof is incomplete or can’t quite get to the inputs that trigger the condition that makes it happen. Some of those tools are really good at finding those, and some of them aren’t, because we talked about all these different kinds of tools and all these different algorithms. Some of them lose so much information that you’re like, “The proof didn’t go through, but I don’t really know where the bug is.” But some of those tools are really good at saying, “Oh, no, here it is,” and showing the crazy path through all the code. Those are harder to argue with.

Yeah, so, you—

But, sorry—

But we interrupted you. So, you were—

No, you please.

Again, I want you guys to do as much of the talking as possible, as long as I can roughly follow it. So, you iterate through this process of defining the spec, and then you’re again iterating through, “Well, here’s why we weren’t able to prove all this stuff.” We’re finding all these edge cases. We’re finding these vulnerabilities. We’re closing those down. Eventually, we sort of get there, and then we’re done, at least for this version or this generation of the system. Now, contrast that to the GenAI case, because we now have an additional level of fuzziness.

By the way, if I could just make one parenthetical statement: this field was proposed by Turing. Turing wrote “Checking a Large Routine,” showing how to do proofs of programs. But this field went into decline in the ’70s and ’80s. It was really only in the monasteries, if you will, where there were people keeping this area alive. It wasn’t really used in practice except for some very obscure cases.

So, it’s become the discipline of the academics. From the academic view, you’re now done, everyone’s happy, and everyone can go celebrate. The problem is that the code, particularly in a cloud world, changes all the time.

So now the big thing is, well, did you do CI/CD? You integrated this into the pipelines, and now you’re trying to repair the proof because the code is constantly evolving. That’s a whole thing that you kind of have to deal with.

They’ve done some really cool work that shows that sometimes the proofs can be automatically updated when the code changes are irrelevant to the main arguments of the proof. The proofs can be automatically updated, and you don’t need to bring the proof engineers back.

Oh, and here’s another beautiful thing: because the tools are actually solving the undecidable or intractable, they sometimes just go to lunch, right? Because the problems are undecidable or intractable, when they give you an answer, now we can believe the answer. But if they don’t—because the problems are undecidable or intractable—sort of, surprise, from time to time they’re just not going to come back because they’re off spinning forever, because the problem’s undecidable or intractable.

Unfortunately, it might be that you changed a variable name from X to Y, and that messed with some hash table deep in the theorem prover. Suddenly, something that took 3 seconds maybe never comes back, or maybe it takes 400 seconds. So now your engineers are like, “Whoa, what happened?” That’s a big challenge for us.

So, again, the generative AI world kind of addresses this in an interesting way. But I’m trying to lay the groundwork for a sort of pre-GenAI world.

Before we get to the GenAI world, in terms of using these methods to help boost the assurances we can get around GenAI systems, how are GenAI systems helping with this work? I understand that we’re seeing all these results in math, which, for somebody who’s not a mathematician, is kind of hard to parse. You’re sort of taking it on faith on Twitter: “Oh, this is a novel problem, but it’s not that big of a novel problem,” or, “The insight here was key,” or it wasn’t key. I don’t really know.

What has your experience been in terms of bringing language models to the process of building out reasoning and these sorts of proofs? Do you want me to say something, Kathleen, or do you want—

I can start. They’re showing a lot of promise. One of the reasons why formal methods was in the monasteries, as Byron was saying, was that it was in the universities. It was only a research problem for a long time. What changed was that it became possible for automation to solve a lot of the problems.

SAT solvers, which was a technology that Byron mentioned earlier, for example, made it so that a lot of the hard work could be done in a completely automated way, which kind of revolutionized a lot of formal methods work. That underlay some of the advances behind the work in HACMS, which started the spiral of, “Oh, actually, formal methods can be used in the real world.” It also underlay what Amazon has been doing.

I think large language models and generative AI have the promise of turning that up to 11 in terms of what can be automated, because language models and generative AI are really good at language, and a lot of formal methods are language-based problems. Formal methods involve fairly sparse languages at the moment. There’s not a massive amount of training data in a lot of formal, model-based languages, but there are places where we can generate the training data and be sure that the training data is correct because we can put it into formal-methods-based tools and get the “Yes, this is good” signal. So, we can turn the crank to generate the training data.

Putting on my DARPA hat—I was the I2O director for 4 years—this is the kind of place where there’s a massive, beating signal that there’s a huge promise: we can get generative AI to be really good at formal-methods-based approaches. We can marry the best of both worlds—generative AI and formal methods—not just code getting generated, but high-quality code getting generated.

That’s a huge promise for the future. Part of why I think one of the things we really want to do is get a high-quality benchmark generated, so that we can measure the quality of code being generated from a formal methods and cybersecurity perspective. Then we can get frontier model companies racing to produce high-quality formal-methods-based code and security code—not just racing to produce code, but racing to produce really good code.

If a lot of the code in the future is going to be written by language models, can we get that code to be really, really good instead of bad code from a cybersecurity perspective or from a formal verification perspective? There’s no reason to think that if it’s going to produce code, we can’t get it to produce memory-safe code, type-safe code, and input-validated code. It’s not going to care. If we could just add the benchmarks and drive the frontier model companies to compete on that dimension, then we can get a future that is much more secure from a cyber perspective.

The threat that we started this conversation with about an hour ago—how AI is going to make the cyber threat much worse—we could tamp down that concern a lot. Byron has been working directly with some of these challenges of getting the frontier models to work better with formal methods, and he can add more details.

To answer your question, I’m going to identify a hierarchy. Imagine you have a program with no loops and no recursion, but you have conditional expressions. Just asking, “Could this conditional expression—if blah, then launch the rockets—” the question of whether the rockets could be launched is an NP-complete problem.

You can put arbitrarily complicated formulae in the if expression, with thousands or millions of propositional variables; you can have integers or whatever. You can put all kinds of crazy stuff in there. And so just finding a satisfying assignment—finding a way to get into that then expression—is NP-complete. Under certain restrictions, like if you choose a language like C, for example, and we're not talking about the heap and a few other things, then it's basically the same question. It is actually the propositional satisfiability question.

That was the first question to be proved NP-complete. So that is an NP-complete question, and when you use propositional satisfiability, you're solving that problem. There has been amazing progress. I first saw this graph in a report, I think, from the HACMS project, where they showed each winner of the International Satisfiability Solving Competition compared on the same hardware and the same benchmarks. It was like, “Wow, they're getting so much better.”

And now we've had really explosive success since then because we've moved from sequential solvers to distributed solvers. There is this really amazing tool called Malibu, which runs many, many SAT solvers across the network, and then they share lemmas as they try to solve the same problem together. That's just unbelievably better. There is a scaling law very similar to transformer models: You put this in, you get this out.

That really explains why we've been so successful at Amazon, for example. It's why we can reason about your policies in your VPC networks in less than 20 seconds now, very reliably. It's because of this success in that area. So that's one piece of the hierarchy.

Now imagine you have loops. You're allowing loops or recursion, but you don't care about anything like “eventually.” You're just saying, “We can't hit this state. We can't hit this state,” like an assert that can never fail. Now you're talking about undecidable problems. To prove that the assert can't fail, you have to find something called an inductive invariant.

It's fundamental. You find this artifact, this weird thing called an inductive invariant, and then you show that it's true when you enter the loop, it's true when you go around the loop, and then you show that thing implies that the assert can't fail. That's what they call safety. It's basically property-based assert verification. That's the next level of the hierarchy.

The next one after that is termination. You say, “This loop eventually terminates.” If you use the word “eventually,” then, generally speaking—there are some side conditions about not having negations and so on—but if you're thinking about the word “eventually,” like, “If I call this API, then eventually I call this other API,” that's ultimately a termination question. To solve that, you need to find something called a ranking function.

To prove termination, you need to find a ranking function, but to prove that the ranking function is a valid one, you also have to find an inductive invariant. To prove the inductive invariant, you also have to do combinatorial reasoning.

The last level of the hierarchy is concurrency. Now we have 2 threads, or N threads, and we're trying to prove things about them. There's a technique called rely-guarantee, where you basically find environment abstractions such that you only have to prove something about each thread at a time. So there are these different levels of abstraction.

I'll now generalize. We have really amazing tools for handling that combinatorial reasoning, that first thing—the no-loops case. But for the tools we had before for reasoning about programs with loops, termination, or rely-guarantee, we had techniques, for sure, but very often the successful way to really make these things work was to just hire a human. So you have a PhD chained to their desk: “Get us our proofs,” right?

There is abstract interpretation, predicate abstraction, and various techniques, but they're limited to certain domains and so on. What's really neat about generative AI is that you can ask it to find these artifacts. You can say to generative AI, “Find me an inductive invariant, find me a ranking function, and find me rely-guarantee constraints such that this whole thing holds.”

All that now reduces just to the combinatorial reasoning, which we have really good tools for. You can iterate the combinatorial reasoning, or the checking, together with the search that the GenAI tools can do. Then you can combine that with all the techniques we had before. Because we're on the cloud, you can run all different combinations of those on different machines and then take the answer you like the most. That really changes the game.

Have you seen examples of this that correspond to, like, move 37 in Go?

The inductive invariants and ranking functions that GenAI tools find are pretty great. Let me—breaking—I realize this breaks the move 37 analogy just a little bit. Basically, to get a proof to go through requires incredible insight, so there are very few people who can find those. You're on the verge of a move 37 miracle every time you get a proof to go through. So, yeah, it's all the time.

What we're finding now is that, in Amazon, the teams that did the scaffolding for proof are now just super happy with GenAI. Now they can pair up a programmer with a generative AI tool. There's a whole methodology being developed in Amazon, and you see this in startups and so on, too, where they're changing their development methodologies to use generative AI to write the code.

The scaffolding they built around the proof provides semantic guardrails that allow them to deploy and not have to roll back very often with generative AI. They're really happy with the investment in it.

What does the GenAI need to see about the codebase to be able to do this?

There's a blog post about this from some folks in Amazon. It works better if you put all the documentation, the threat models, and everything else in the same place. That way, when the generative AI is generating the code or finding the proof, it also has the documentation, the ops plan, and everything else they've written.

If you throw that all in, it's actually better able to find the code. It sees the entire codebase, and it also has all the thinking about the codebase and all the documentation. That's really cool: It has not just the code, but also the human-level understanding of the code.

For proof search, you can ask, “How do humans do proofs?” They often read a bunch of other proofs. Then they're essentially doing matrix multiplications in their head to derive something like, “This proof looks a lot like this thing, but it's a little different. It's like this other thing. So I bet this is the inductive invariant.” They pull it out like a rabbit out of a hat, and voilà, the thing goes through.

People are really good at that, like John Harrison. He's read all the proofs. The generative AI can do that, too. You can actually pass it old proofs of programs, and it's going to be better at finding new proofs. It reads old proofs.

Yeah, you can do that.

It reads proofs of software construction and digests all of the literature about how you prove these kinds of things. Most model providers today are training their models over proofs, like in Lean, for example. So they actually understand some of those old proofs. You can also provide your code and proofs you've done into the context window.

So do I understand the path from here? This has obviously been a huge critique of AI-generated code: It's insecure, right? We've heard that all over the place, and I think not incorrectly, at least so far.

If I am understanding correctly, the vision for getting to a world where AIs generate secure code at a much higher rate is basically that, first, we're taking advantage of a pretty familiar trick: Something might be hard to come up with the proof for, but it's easy to verify the proof, right? That's a cornerstone of this.

The AIs are presumably at least in the game now. Based on all this pretraining and other things they've learned, and all the proofs they've read, they're able to have some nonzero hit rate. You have to run your AIs, especially in the beginning, when you're just starting to spin the centrifuge. You have to run them a lot and have a high failure rate, but you get some successes.

Those successes can fold back into the training data. With that overall flywheel starting to turn, we're now getting the AIs to be quite good at the proofs. Then we can apply that proof capacity as a reward signal to the coding problem itself. Downstream, we're now rewarding the core coding objective in part based on correctness as evaluated by these proofs.

So we've got a sort of multi-AI, multiple roles for AI in kind of bootstrapping this thing into success. I think it's easier to help developers encode into linear temporal logic what they mean by “all data at rest is encrypted” than it is to encode the Family and Medical Leave Act. Right? It's much smaller in scope. [laughter]

Now we have these tools that are already doing what you call auto-formalization from natural language to logic, so we can deploy those tools in these domains. It makes it remarkably easier.

Yeah. So we can envision a world over a generation or 2 of future models where, as long as this is prioritized, given what we're already seeing in terms of logical reasoning ability, mathematical ability, and coding ability, doesn't it stand to reason for you that GPT-6 and Gemini 4 should be basically superhuman in their ability to write secure code the first time? Is that where we're headed?

Yes, and also Nova and the open-weight models, yes. [laughter] So, yeah, I think we're there. I mean, we're seeing that right now, and there are open math conjectures—last week, there were open problems proved. We're quickly heading there already.

We need to incentivize the production of good code and not bad code, and I do think that we need to not just create the capacity for good code; we need to move away from bad code. I think that we're likely to see increasing incidences of cyberattacks that would create the motivation to get rid of the bad. I guess we need to incentivize the creation of good code, disincentivize the creation of bad code, and then incentivize the use of good code to replace the pervasive bad code in our critical infrastructure, et cetera, so that society is much less vulnerable to cyberattack than we currently are.

And the good news is, there are tools to help you translate your code, right?

Right. Generative AI can help you move from one system to another, so you can upgrade your versions of your language and then enjoy the benefits of the fixes in the runtime of the new version of the language. One of the easiest things to do in formal methods is actually prove the equivalence between 2 programs, because now you have a spec. Showing that one version of the program implements the same thing as the other program is something that we can do.

Often, when you're updating, you're moving from Java to Rust, for example, so there's a little bit of work to make sure you got the semantics of Rust and Java right. Often, people use different APIs, and it's a little harder to do that mapping, but it's much easier to move between APIs and languages now than it used to be, so that's also good news for security.

Like C to Rust, DARPA has a program called TRACTOR, which is about automatically translating from C to idiomatic Rust. That's about moving from a non-memory-safe to a memory-safe language, which is about establishing and maintaining the property that memory is safe. It's the abstraction that you intended: when you stored something in memory, it stayed the way you intended it to be.

I guess we're really hitting our stride now. I sometimes try to coin these phrases, like “the great implementation” was sort of my phrase for: we're going to unbundle jobs into tasks and get AIs to do all these tasks. We'll sort of implement AI in all these different corners of society. Here, I'm getting the sense that there's a great verification, or a great rewrite, if not full verification.

What are the next few years like? How fast do you think this needs to happen? It seems like it might need to happen pretty fast if we really want to be secure before the bad actors are using the same capabilities to break into all the critical infrastructure. What is this next period of time? How long is the period of time, and what does it look like when we need to go through, I don't know, 60 years' worth of software and fix all these holes that our feeble human minds have left us with?

I think that's a question of motivation more than a question of technology, right? We're seeing, with the results of the AICC cyber competition, that AI plus cyber could find and fix bugs at speed and scale. Google released the CodeMender project; OpenAI has a similar thing, right? What we've been talking about is really showing a promise that AI-enabled code generation can rewrite code at speed and scale to a much higher standard of correctness in the relatively short term.

The way AI is improving so fast, this is just going to be the worst it's ever going to be: where we are right now. And I think that the conversation we started out with—which was that AI is going to be enabling cyberattackers at all levels of skill, at all parts of the cyberattack chain—means that the level of attacks is just going to increase.

That said, the statement that cyberattacks are increasing in severity has been true for the past, I don't know, 20 years, and we've just been like the frog getting boiled. We keep getting boiled, and we haven't responded yet, so I don't know when we're going to be like, “Holy crap, we actually need to do this now.”

Right? The capabilities are there, the tools are there. When the Y2K date problem came around, society did mobilize and did go and fix those bugs, right? So there wasn't a huge problem when the year 2000 rolled around and all of the dates that were stored in 2 digits suddenly meant something completely wonky. So I don't know when we're going to be motivated enough to use these technologies. I think the technology will be there when we get serious about doing it.

What's your sense, Byron?

I think the commercial marketplace kind of drives this, right? So how much are people willing to put up with, and how much are they willing to pay for their infrastructure? I personally choose my machines and phones based on their reputation for security. Certain makers of machines and phones take it more seriously than others, and I pay a little bit of a premium for that. I would continue to do so and would advise others to do so.

I think that the cost and difficulty of these tools is dropping pretty substantially. I'm seeing that at Amazon. The teams that previously couldn't have used these tools—I mean, teams in Amazon also have different threat models than others, and so for some teams, these tools are really appropriate, and for other teams, they're a little less so. There are teams that choose not to use formal methods and some teams that do. That barrier to entry is going down, so those teams that weren't using them before are beginning to adopt them now.

I think that will continue to happen, and then there's a big commercial push. Amazon released the Kira IDE, and its big differentiator is that it's specification-driven. There are companies trying to innovate and make products, and this is a new dimension in which to innovate. If those products are successful and people flock to them because of their capabilities, then that flywheel will drive things.

So I'm actually fairly optimistic. If you look at agentic AI, it's kind of a way of saying we're doing declarative programming. If you look at AgentCore Policy, which we announced last week at re:Invent, it's a Cedar formal specification over the envelope of what you're okay with an agent doing and not doing. That gives you a new way to declaratively specify what the systems can do.

I think that society is also beginning to appreciate, through the lens of generative AI, the notion of declarative programming as opposed to imperative programming. I think that will change how programs are written and will have different threat vectors, and we'll have to figure that out as we go along. It's pretty unstable, as far as I can tell, but I think that I'm no less worried now than I was 10 years ago. I'll say it that way.

Okay, well, [snorts] hopefully the next year will bring some progress. Okay, so I think I have maybe 3 more questions. They're all kind of substantial; hopefully, we can get all 3 of them at least partially answered.

I guess one is: how far does this go? How long does it take, and how far does it go? If we said as a society, “Okay, we're going to stop writing new software. We're going to do the great rewrite. Here's all the formal tools that we have and the language models that can help you maximize their use and rewrite stuff,” how long do you think that would take, and how far could we get?

There are, as you well know, many other approaches, including companies that are trying to create AI hackers to go find the vulnerabilities. Could we get to a world where those strategies are rendered unnecessary because we're just so confident everything is kind of buttoned up that we don't need an AI agent to go poking around to try to find vulnerabilities? That's sort of imitating the old human way of poking and clicking and finding things and then coming back and saying, “Okay, I found something. Now we can fix it.”

Could we ever get to a point where we don't need to do that anymore because the whole system broadly has become sufficiently robust, or is that too pie in the sky? Do you think we'll always kind of have to have these different angles of attack on the problem?

I think belt and suspenders is a fine idea.

I think it doesn't hurt very much to have AI bug-finding systems poking around, but I think you could get to a place where they weren't finding things very often. We talked about how you have people, software, and hardware. I think we can get to a place where the hardware and the people are the source of almost all of the vulnerabilities in the not-too-distant future if we went all in fixing the software.

Yeah, that's really interesting. One of the big worries, of course, with AI broadly is what happens if the AI gets out of control, without digressing into how plausible that is. I'm always on the lookout for any sort of theory that could really work, and this seems like one line of attack where you could imagine getting to a sufficiently high level of assurance that you could say, “Look, the AI isn't going to be able to hack its way out of this box because we've done this level of assurance, and we can at least take that self-exfiltration risk off the table.”

So my answer is that I find every safety technology just allows us to push even harder. I think we drive faster because our cars are safer. The commercial marketplace also drives features and speed and all these kinds of things.

I remember I worked for a company that had device drivers in user space, but because some games were slower, they moved the device drivers into kernel space. So they lost the protection. Then video device drivers just weren't checking error conditions. If the operating system failed to allocate memory to you, they just didn't care because they wanted to be high-performance in the common case.

So I think there's also a balance with availability and features. The commercial marketplace has a bunch of dimensions, and they're navigating that. They're not going all in for security.

Yeah, I 100% agree with Byron. If you were 100% focused on sandboxing a super-aggressive AI, formal methods would have things to help with. It would help with that. That's literally the meeting I was having before this call. The frontier is virtualization, sandboxing, and policies for AI. That's where we're pushing right now: sandboxing superintelligence. That's crazy, but that's kind of where we might need to go.

How about, in closing, let's go back to the automated reasoning checks? The most common profile of listener to this feed, as far as I can tell, is the AI engineer. If you're somebody building generative AI solutions for businesses, maybe give me a little bit more of the pitch: what kinds of problems can they solve, and what kinds of things can they take to their stakeholders and say, “Hey, if we use automated reasoning checks, we can be sure, to a certain level of confidence at least, that we're going to implement the family-leave policy correctly”?

Then I want to do one more thing on that, just to zoom out a little bit on the societal question of how you envision this existing. I think a lot of things right now, society's wheels are greased a little bit by the fact that people can go off policy a little bit. Maybe you don't quite qualify for the family leave, but we'll make it work in this case because you've been a long-tenured employee or whatever.

One could argue that's because the rules often have different interpretations. We have sociotechnical mechanisms right now. For example, if you want to build an accessory dwelling unit in Portland, Oregon—a small house in your backyard—what are you going to do? You're going to file with the city, and someone is going to look at it. To be successful there, you're probably advised to get an architect, and probably an architect who works in Portland, Oregon, not Portland, Maine, because the rules are going to be different.

That feedback mechanism raises the question: how do you know that the architect really solved for the best? There are various setback rules. If the house is a certain height, it needs to be 5 feet away from the property line, but if it's this other property, you can be right up against the property line. How do you know they got that all right? How do you know they didn't maximize what you see? You're using these intermediaries through the sociotechnical mechanisms.

I think the dream of AI—and its current failure—is that it has not been able to deliver on the ability for people to democratize access to information because of incorrectness due to hallucination. No one is going to use a transformer-based language model, ask it about the city of Portland's zoning rules, and then just start digging and building a house. They're ultimately going to have a bunch of people look at it because they don't believe it; they don't trust it.

It's tantalizingly close to allowing everyone to have access to information anytime—24/7, super-fast, and super-cheap—which democratizes access to information. It's not just for rich people who can hire an architect. To do that, we need to do the last mile. We need to make the answers actually correct, and automated reasoning checks are designed to fill that gap.

It's not creative at all. It merely defines the envelope of true and untrue answers, and it uses logic to define that infinite space. Then it allows the language model to be as creative as it wants, but it's going to map it back over to logic and prove or disprove that according to the rules.

One can imagine that these rules are open-sourced or provided by the city. There could be various models—maybe they're licensed, maybe different organizations provide their rules—and you can conjoin them. There are various models that are possible, but I think it gives access to accurate information about what's true and untrue. It also gives us an ability to argue with it, to say, “It's this axiom that makes this rule unfair.”

Then you can discuss, as a society or an organization, whether we should change this rule. You could save all the past interactions, propose changing the rule, and replay those chats to see if you're going to be happy with the differences. So it gives us tools, as a society and as organizations, to appreciate what our rules are, who they impact, and to rationalize those rules.

My hope and belief is that people will now have a much nicer way of pushing back against the rules rather than just cheating.

Well, I think it's an interesting question: where does the wiggle room come in? What are the rules where this one absolutely can't be fudged, and this one should have wiggle room? Where does the judgment get to come in? Does the large language model get to provide judgment, or is the judgment at a higher level—actually going and talking to a person? Or is there no slack or judgment?

The other thing is that not all axioms are equivalent. You can do proofs under certain axioms or certain axiomatizations, and then you can add other ones that are like second-class citizens: these are the ones we'd like to avoid, but if the only way to get to that answer is to use this one, that's fine. The final one could be, “Go talk to a human.”

What does Steve say? That can be the last axiom: Steve agrees, then okay, great. That allows us to fudge things, but—

Get-out-of-jail-free card. Yeah, interesting. I find the promise of the scalability and speed of all these things incredible. Talk about wanting to get to some sort of housing abundance: the ability to expedite so much stuff in the case that you outlined there is incredible. The fairness would presumably be dramatically improved.

And then I do wonder what new mechanisms we will also need to put in place around this. I think Europe is doing some of this stuff with a right to appeal to a human. We don't have that stuff in the US yet, but we might come to need it.

But there is also a societal marketplace. I have moved countries to get access to resources I didn't have in the other country. People move with their feet a little bit. It may be that certain countries regulate in ways that slow things down, add cost, and add latency. Other countries may regulate in a way that makes a lot of sense: it provides fairness or transparency, but also speeds things up.

Those countries will have faster growth, or they'll meet the goals of the society. Other countries will see those countries succeeding and maybe change their regulations. So I think we're all trying to figure out how to work with these tools, but there are a lot of things that can be good, and then there are risks, and we need to figure out as a society how to deal with them.

I mean, sometimes human judgment is good. It adds flexibility that clearly should be there. And other times, human judgment is bad because it adds bias.

Yeah, exactly. And in a way that can torch the process in a way that’s bad.

Yeah. Yeah, definitely. No easy answers. I think that’s a constant theme of The Cognitive Revolution as a whole. The big challenge for society is that we’re learning how hard it is to figure out what truth is.

Well, that’s all I had. Do you guys want to maybe each give one closing thought or touch on anything we haven’t touched on, keeping in mind the sort of AI engineer profile? If there’s anything else you would want to impart or a call to action, or even just a pitch for the product, one more pitch for the product would be welcome, too. And we can leave it there.

Yeah, so I’ll start. There’s this notion of neurosymbolic AI, which is the combination of the automated reasoning we’ve been talking quite a bit about, but also the cognitive techniques. I think much of the magic is at the intersection. How do you do inference, reasoning over nondeterministic automata at the same time?

I think it’s a peanut butter-and-chocolate moment where, if the two are combined, they really have a multiplicative effect on each other. Traditionally, there have been silos: there have been automated reasoning and formal methods nerds, and then there are the nerds who work on statistical approaches. They kind of didn’t speak the same language; they didn’t go to the same conferences.

I think what’s amazing right now is that those areas are kind of blurring back together in a way that was envisioned in the early ’50s, and it’s a pretty exciting time.

Yeah, I would say the same thing. Formal methods and AI are two great tastes that go better together. They have different strengths and weaknesses, right? Formal methods give you guarantees but are not very flexible and are hard to use, and AI is very flexible and easy to use but often not trustworthy.

So, if we can figure out how to put them together, you can get the best of both worlds. DARPA’s I2O has a number of programs that are exploring different combinations of using those technologies to get exactly that—the best of both worlds. I mean, there are lots of different ways of combining them, and the magic is in exactly what combination, in what circumstance, to get exactly that: the chocolate and peanut butter.

Yeah, love it. That’s an inspiring vision. I really like it. I’ve got a lot more to learn, as you guys can tell from my baseline coming into this conversation, but I really appreciate you both for taking the time to educate me and all of us. Kathleen Fisher, Byron Cook, thank you for being part of The Cognitive Revolution.

Thank you.