# You Don't Trust AI. So Why Are You Shipping Its Code? URL: https://securitytable.ai/you-don-t-trust-ai-so-why-are-you-shipping-its-code/ Published: 2026-11-04 Duration: 3004 seconds Season: 4 Episode: 26 Hosts: Chris Romeo, Izar Tarandach, Matt Coles ## Show notes and chapters Sam Altman told a Stanford audience he no longer thinks we can just patch all the bugs, and the AI Security Table can't agree on whether that is news. Chris argues a swarm of subagents can tear through a repo and drive defects way down, while Matt counters that every system ships with defects and always will, so the real limit is cost, now measured in tokens. Izar warns that tokens are just the new regex, the latest silver bullet in a long line of them. Then the hosts dig into Anthropic's work using Claude to write Rocq proofs for 123 open source libraries, and argue over what a proof actually guarantees, who checks a model that writes both the patch and the proof, and whether compounded mistrust ever adds up to trust. Izar gets the last word: LLMs are not compilers, so stop treating them like one. Mentioned in this Episode: ➜ [Sam Altman: 'I No Longer Think We're Gonna Be Able to Just Patch All the Bugs'](https://gizmodo.com/sam-altman-i-no-longer-think-were-gonna-be-able-to-just-patch-all-the-bugs-2000829947) ➜ [LLMs are making formal software verification feasible at a much larger scale](https://www.anthropic.com/research/formal-verification) ➜ [seL4](https://sel4.systems/) ➜ [The Rocq Prover](https://rocq-prover.org/) ➜ [OSS-Fuzz](https://google.github.io/oss-fuzz/) Chapters: 00:00:00 - Cold Open: Privacy Thought of the Day 00:01:35 - Article Intro: Altman Can't Patch All the Bugs 00:02:22 - Izar Reads the Altman Quote 00:03:07 - How Many Bugs Are in Your Software? 00:04:07 - Chris's Case: 200 Subagents on One Repo 00:05:49 - Matt's Case: We Always Ship With Defects 00:06:54 - The Disposable Software Argument 00:08:15 - Nobody Saw the Exponential 00:10:12 - The Token Cost of Hidden Criticals 00:11:55 - Izar's Rebuttal: Tokens Are the New Regex 00:13:33 - Defenders Finally Have an Advantage 00:15:16 - The Knowledge Pyramid 00:16:57 - We Only Talk About Superintelligence 00:18:16 - Article Intro: AI and Formal Verification 00:19:53 - Izar: Proofs Nobody Can Read 00:20:50 - Matt: Start With Something Small 00:22:01 - The Proof Gets Bigger Than the Code 00:25:12 - Correctness Is Not Security 00:26:53 - Verified Blocks, Untrusted Integration 00:27:57 - Verifying the seL4 Microkernel 00:29:02 - What Was Actually Verified? 00:30:47 - Fuzzing and the Next Byte 00:31:56 - The Article's Limitations 00:33:25 - Who Is Actually Doing the Proving? 00:34:19 - 123 Libraries and 600,000 Line Proofs 00:35:57 - How Is My Morning Any Better? 00:36:42 - Memory Safe Languages Already Exist 00:37:43 - Should Claude Write Its Own Proofs? 00:39:04 - One Frontier Model Checks Another 00:39:52 - Does Compounded Mistrust Equal Trust? 00:41:24 - Use AI With Enough Mistrust 00:42:17 - How Much AI Code Did You Review? 00:44:07 - Back to Threat Modeling 00:44:37 - Feeding Knowledge Back to Agents 00:46:25 - Secure Coding Standards Never Worked 00:48:11 - Closing Statements: LLMs Are Not Compilers 00:48:40 - Outro Follow AI Security Table: ➜ Home: [https://securitytable.ai/](https://securitytable.ai/) ➜ X: [https://x.com/AISecurityTable](https://x.com/AISecurityTable) ➜ LinkedIn: [https://www.linkedin.com/company/ai-security-table/](https://www.linkedin.com/company/ai-security-table/) ➜ YouTube: [https://www.youtube.com/@AISecurityTable](https://www.youtube.com/@AISecurityTable) ## Transcript **Izar Tarandach (0:09)**: If my thoughts about privacy are secret, do they still count as private? **Chris Romeo (0:14)**: And folks, welcome to the AI Security Table, and that's your thought of the day. So please ponder that throughout the day. If your thoughts about privacy are private. Are they still private privacy thoughts about privacy? Try to put that together all at once. **Izar Tarandach (0:34)**: If a private tree falls in the middle of the forest and there's nobody around to sell it to a data broker, does it count as confidential? **Chris Romeo (0:43)**: Yes and no. **Matt Coles (0:46)**: What happens if a hiker comes and finds it later? **Izar Tarandach (0:50)**: What's the sound of half privacy? **Chris Romeo (0:53)**: Half privacy. **Matt Coles (0:55)**: Half privacy. Is that a half open connection? **Izar Tarandach (0:58)**: I'm doing privacy cons here. **Chris Romeo (1:01)**: Privacy. You're trying to con people out of privacy? **Izar Tarandach (1:03)**: No, that's a data broker. **Chris Romeo (1:05)**: I couldn't resist. I'm sorry. It's early **Izar Tarandach (1:07)**: in the morning. **Matt Coles (1:08)**: That's a data broker. The analogies are, and the metaphors are— **Chris Romeo (1:11)**: We are all semi-caffeinated here at the AI security table. **Matt Coles (1:16)**: Wait, we are? Oh yeah. One of us is caffeinated, therefore semi. **Chris Romeo (1:19)**: Semi. **Matt Coles (1:20)**: One of us. One of us. One of us. **Chris Romeo (1:22)**: We'll let you you know, just try to decide which one is overcaffeinated, which two are undercaffeinated. **Izar Tarandach (1:32)**: There's no such thing as overcaffeinated. **Chris Romeo (1:35)**: That's true. All right, let's, so let's deal with this one that you did, this issue that you just threw freshly into, onto the table here about Sam Altman from OpenAI making some statements about We're not worthy. **Izar Tarandach (1:52)**: We're not worthy. **Chris Romeo (1:54)**: Nah, we are. Don't, don't even go there. Let's, let's not put these, these folks on a pedestal like everybody else in our industry does. They're not. **Izar Tarandach (2:02)**: What? But I thought that that was the rule. **Chris Romeo (2:05)**: No. **Izar Tarandach (2:06)**: No? **Chris Romeo (2:07)**: You know, on this podcast, we break all the rules. We're the bad boys of application security. I couldn't even say it. I couldn't even say it with a confident **Izar Tarandach (2:20)**: measure. Where's my buzzer? Okay. So what is it that the guy said? I no longer think we're going to be able to just patch all the bugs, he told the audience, in part due to the ongoing advancement of AI models and in part because the targets of cyberattacks have acted too slowly to get ahead of it. **Chris Romeo (2:40)**: Ouch. Gut punch. **Izar Tarandach (2:41)**: It's like you're standing in San Francisco in the middle of the street and you're seeing the tram coming down. And you can clearly see on top of the tram written security debt. And all of a sudden the thing just goes and hits you. All of a sudden, like nobody saw it coming. **Matt Coles (3:00)**: I actually agree with his statement a little bit. **Chris Romeo (3:03)**: What? Come on. All right. Explain. **Matt Coles (3:07)**: How many issues do you think you have in any given piece of software? **Chris Romeo (3:11)**: How large of a piece of software are we talking about? 10 lines or 10 million? **Matt Coles (3:17)**: No, let's say a common desktop application. So probably 100,000 lines of code. **Izar Tarandach (3:23)**: Sure. **Chris Romeo (3:23)**: How many security? So how many flaws? **Matt Coles (3:27)**: How many flaws? Now here's the interesting question. Not necessarily a vulnerability, but a thing that can be exploited later. **Chris Romeo (3:34)**: Okay. I just got into a big argument on LinkedIn about this one, so I can't wait. **Izar Tarandach (3:39)**: Where later is a movie target. **Matt Coles (3:41)**: Right. And, and this is, this is part of the problem, right? Is you're always gonna be chasing your tails. We're always chasing our tails anyway in software security, right? Cuz we developers introduce bugs and then they get, there's a risk process where those bugs get shipped. **Chris Romeo (3:57)**: Yes. Right. **Matt Coles (3:58)**: We don't ship, we don't fix all of them. **Chris Romeo (3:59)**: You're describing the, the, the distant past, not the current future that we exist in here where I can, I can spin up 200 subagents and say, Tear this repo up, try find as many flaws as you possibly can and fix them. **Izar Tarandach (4:18)**: And how many do you still have left? **Chris Romeo (4:21)**: It'll be less than what I started with. I hope. **Matt Coles (4:24)**: Are you sure? **Izar Tarandach (4:25)**: Are you sure? **Chris Romeo (4:26)**: Well, it, it, it come, but it come. If, if you do this from a single model, single agent perspective. Then yes, you will likely not get any type of positive result. If you use a multi-model, multi-provider approach to looking at your 100,000 lines of code, you can reduce, maybe not to zero, right? But you can reduce, but we'll get into formal methods and formal verification later. **Matt Coles (4:58)**: Yeah, we got to talk about that next. **Chris Romeo (4:59)**: 'Cause that could get us to zero, maybe. But yeah, my point is like, you can eliminate some percentage, I think some large percentage of them by having the right strategy of models and reasoning and capability of the models. **Matt Coles (5:16)**: Sure. And how many, how many software vendors are going to do that on day one, release one of their thing? **Chris Romeo (5:24)**: Well, a bunch of people that used PHP in the last week or two have been scrambling to try to update that sucker. **Izar Tarandach (5:32)**: Yeah, that's the point. Very quickly. You do all that nice exercise with your codebase, and then Carl goes and changes a little library written somewhere else by somebody completely different, and pop goes the weasel. **Matt Coles (5:47)**: Right. So, we're in the same boat, right? That we've been in for decades is software gets shipped. And I won't— well, let's not restrict us to software, by the way. It's systems get shipped, right? They get built, release one, they have a bunch of They have stuff in them. They're not perfect and we're okay with that, right? We know bugs exist, bugs happen. **Chris Romeo (6:04)**: We're not okay with it, but we just have to accept it. **Matt Coles (6:06)**: We have to accept it. Right. And whether it's human-generated code or if it's AI-generated code, and certainly you can do things with, with, you know, verifications and QA and whatnot to try and reduce the level of defects, but we almost certainly are going to ship with defects and we're certainly going to ship with things that will later become defects. As we all know, right? Zero days exist. **Chris Romeo (6:29)**: So for now, I would agree with your statement today. I don't know. I don't agree with your statement one year and five years in the future. **Matt Coles (6:37)**: But if we start right, but if we start fresh, then what you're saying makes sense. And that's, I think, where Sam Altman is going with this, right? Is now that we have the power to build it correctly, shouldn't we go back to release one? **Izar Tarandach (6:52)**: But do we? **Chris Romeo (6:55)**: So you think he's taking the disposable software argument? **Matt Coles (6:59)**: I think he is. **Izar Tarandach (6:59)**: No, he, he's saying, he's saying this. **Chris Romeo (7:00)**: I didn't get that from it, which I've heard people describe the disposable software argument for the future, which is we'll reach a point where it won't even make sense to patch something. You just have the agent rewrite it from scratch. That's right. **Matt Coles (7:15)**: I, I don't think that's, I don't think that's in the far, far distant future. **Izar Tarandach (7:19)**: Look, he's just being the hero that we didn't know we needed, right? **Chris Romeo (7:24)**: You cannot attribute him to Batman. No, he is not Batman. No, I refuse. I refuse to accept that. **Izar Tarandach (7:31)**: Wait, **Chris Romeo (7:32)**: where's my button to bleep? Do I have a bleep button so I can just bleep these out from now on? **Izar Tarandach (7:36)**: His next quote. **Matt Coles (7:37)**: Don't we have time delay? **Chris Romeo (7:39)**: We are time delayed because we're on broadcast television. **Izar Tarandach (7:43)**: This cybersecurity dot dot dot. I don't even know a dramatic enough word to use, but the problem coming towards us, I think, is still something that we have not, as organizational leaders or countries or individuals, taken seriously. **Chris Romeo (7:58)**: I agree with the dog. **Izar Tarandach (7:59)**: And the dog appears to agree with him, which is basically what we've been saying for the past, I don't know how many, 30 years. **Chris Romeo (8:05)**: Well, yes. I mean, it's tough to, it's tough to argue with that statement that leadership across small and large companies haven't taken cybersecurity seriously. **Izar Tarandach (8:15)**: Agreed. But then, then he throws in the, the, the, the Facebook lingo, whatever. People definitely patched some bugs, but it was another one of those cases where people didn't really intuit the exponential. **Chris Romeo (8:29)**: What? What does that mean? Did a model write this? No. Is that actually him? **Izar Tarandach (8:33)**: They, they, they, they didn't see the curve going up fast enough, you know? Even though we were standing at the bottom of the curve saying, look at that mother going up. **Chris Romeo (8:43)**: Yeah. **Izar Tarandach (8:43)**: Apparently nobody else. **Chris Romeo (8:45)**: It was, it's all, it's all perception. Because we were seeing it, we were watching it. **Izar Tarandach (8:50)**: We were surfing that shit, that thing. **Matt Coles (8:54)**: There goes our PG rating again. **Izar Tarandach (8:55)**: Indeed. **Chris Romeo (8:56)**: So much about E for Everyone. I thought that was always my, our goal. Yeah. So I, I, I think it is, I think this is, this is something we have to focus on right now. The ability to use AI to remove as many latent flaws as we possibly can from a codebase. **Izar Tarandach (9:16)**: Yeah, but look, the conversation will always be, until we get to the formal methods, did you do a good enough job, right? When you have on one side a tool that apparently is able to intuit the exponential and figure out every single hairy issue that we can, could never with our measly scanners. Right? Or even reading the code. Sure, it's going to figure out a bunch of low-hanging fruit, medium-hanging fruit, even some high-hanging fruit. **Chris Romeo (9:52)**: Some critical. **Izar Tarandach (9:53)**: But then what you're left with is the hidden critical, which could, maybe not, have the biggest impact. **Chris Romeo (10:04)**: Well, you just have to find ways. For the model to find these hidden criticals. **Matt Coles (10:12)**: Part of the problem is costs. And I don't mean, well, it translates to dollar cost, right? But in order to find more higher complexity of problems, right? So the low-hanging fruit of the flaw in the code that's obvious, right? Like it's a CWE written right there, right? I don't check memory, or I have some other flaw that's obviously a single weakness, right? That's a grep. I mean, it's not a grep, but it's a grep, right? It's, you're looking for a construct in code. As you get more and more complex, and as you start to chain these things together, the token cost goes up, right? **Chris Romeo (10:52)**: Well, who cares about the cost? **Izar Tarandach (10:54)**: We're **Chris Romeo (10:54)**: fighting for security. We're fighting for security. **Matt Coles (10:57)**: Somebody cares about the cost and we're back to the iron triangle problem. **Chris Romeo (11:00)**: It depends on. It depends on the organization. So I'm aware, I was talking to somebody who's at a, I would say a very high-end, and not even a startup anymore. It's a company that's now established, but a tech player, not in the AI space. And they were given a blank check by their CEO. The security team was given a blank check for token spend. CEO said, I don't care, just reduce my overall risk profile. **Matt Coles (11:29)**: Right. Of the, of the million or so software vendors in the world today. Yeah. How many of them are gonna do that? **Izar Tarandach (11:36)**: Less than a hand. But here's the problem. We, we are— **Chris Romeo (11:39)**: doesn't wanna succeed. **Izar Tarandach (11:40)**: Wait, we, we are falling into the same pattern. **Matt Coles (11:42)**: Maybe it's pay to play. Is that what you're saying? It always has been, by the way. I mean, you've hired the, the good engineers or the biggest tools. **Chris Romeo (11:49)**: Yeah. Look at the Frontier Labs now. **Izar Tarandach (11:51)**: Guys, wait, wait, wait, wait. **Chris Romeo (11:51)**: You get hired there, you're like, oh, look, I'm making $5 million a year. Sweet. **Izar Tarandach (11:55)**: Wait, you, you, you fall into the same patterns that we've, that we've fallen in the past, right? **Chris Romeo (12:01)**: Guilty. **Izar Tarandach (12:01)**: We are going, we are now saying tokens, tokens is everything. Once upon a time we said regular expressions was everything. Once upon a time we said AST trees was everything. **Chris Romeo (12:10)**: Anyone who's ever created a regular expression that's more than 5 lines did not say this was everything. They said this is terrible. **Izar Tarandach (12:16)**: But everybody was like, oh, we're going to write the scanner and figure out all the bugs. Just go back 10 years and look at the marketing that we got from, from companies. **Matt Coles (12:24)**: Oh, sure. **Izar Tarandach (12:25)**: And now we are saying tools are everything. But they're not. Sorry, not tools. They are everything. But they're not. They're limited. We know they're limited. Sometimes it can even be proven that they're limited for some cases, right? So let's not step into the same mine that we keep telling people that they step on. Let's not just call the next Messiah and say this one is going to take us out of of the sense. And then they're good. **Chris Romeo (12:54)**: So what else can we do then? What should we do? Just, just wait. **Izar Tarandach (12:59)**: Let's bring everything together. No, let's bring the tools together. Let's get a bit of this one, a bit of that one, a bit of that one, the best of all of them. Make them work together and then see what we get out of it. **Chris Romeo (13:09)**: If you don't go all in, let me, let me throw the other side of the table here. If you don't go all in on models, LLMs, AI, assisting your security program. We're, we're watching the other side go all in with AI, meaning the attacker collectives of the world. **Izar Tarandach (13:32)**: Yeah, but some of the— **Matt Coles (13:33)**: So the defenders have, defenders now have an advantage in this area because the tools that were deterministic in the past were always generating a lot of good information. I'm sorry, they're always generating a lot of information. The problem was good information. And what the AI is, I think, really going to help us with, or should help us with, is in the past you used to have humans, you'd have a team of engineers go look at 100,000 findings from your static code analyzer and go, "Ah, that's a lot of stuff. Ship it," right? Because it was noise, but it wasn't really noise. It was actually a lot of good data points. **Chris Romeo (14:13)**: Well, it was a lot of false positives too, though. **Matt Coles (14:15)**: Yeah, but it was a lot of false positives under certain condi— under a certain condition, which the engineer was biased towards. Now, I think what we might see is that these findings are valid, or they're valid under certain conditions that the models can now extend to multiple path to tech discovery. **Chris Romeo (14:34)**: The model's working with the output of a deterministic scanner. Should be able to get you better detection of false positives, reachability, all these types of things. **Matt Coles (14:47)**: So I'm going to liken this to when we went from, you know, point-and-shoot security testing to, to aggressive fuzzing. **Izar Tarandach (14:58)**: He's reviving DAST. He's reviving DAST. I can see it. **Chris Romeo (15:01)**: I'm not reviving DAST. He loves DAST. **Izar Tarandach (15:04)**: I am not. **Chris Romeo (15:04)**: This is time he's been wearing a t-shirt under his jacket that says DAST is the science. **Izar Tarandach (15:09)**: He's doing CPR on DAST. **Chris Romeo (15:12)**: And it's, he, he was afraid to speak because we were so mean to the DAST community. **Izar Tarandach (15:17)**: Actually, Matt, I think that what you're describing is a journey into what's called the knowledge pyramid or information hierarchy, right? **Chris Romeo (15:26)**: What is this, a CISSP review class? **Izar Tarandach (15:29)**: No, no, no, no. It starts with Data in the bottom, it goes up one level to information, another level to knowledge, another level to wisdom. So we had a lot of data in the form of code. This is our data. This is what we swim in. We applied the scanners. We got a lot of information. Then we had to figure out of all this information, what the heck is good? What is bad? **Matt Coles (15:54)**: Right. **Izar Tarandach (15:54)**: That was transforming that information into knowledge. Now we know what's bad. We know what needs to be fixed. Then from knowledge, we would go to, okay, what are the mistakes that I can't repeat again? And here's my guidance and here's my templates and all that good stuff. And that became wisdom. And that journey took a lot of time because you had a lot of data, you still had a lot of information. It was hard to come up with the knowledge and only sometimes you could get to wisdom and then you had to go back to the people who created the data and apply all that., right? And that loop was hard as **Matt Coles (16:29)**: hell, **Izar Tarandach (16:29)**: right? Especially the one going from knowledge to wisdom, **Matt Coles (16:32)**: right? Because you had a lot of, again, you had, you had people, which isn't necessarily a problem, but there's bias, there's schedules, there's cost, there's, there's people. **Chris Romeo (16:43)**: I'm just, I'm just pissed. I'm realizing I'm just pissing everybody off today. Sure. I'm just, I'm in one of those— **Matt Coles (16:48)**: You're not pissing us off. You're just, you're just arguing about, uh, invalidity. **Chris Romeo (16:51)**: I mean, every— I'm trying to, I'm like, I'm like equal opportunity offender this morning of like, **Matt Coles (16:57)**: Democracy. So, but AI models are, well, since we've talked, we can talk about superintelligence if we want. **Chris Romeo (17:04)**: We talked about that last week. That was last week. We already, we already, we already handled superintelligence. **Izar Tarandach (17:10)**: Kill me, kill me in the morning. Kill me in the morning. Yeah. Yeah. Why not? It's not like I have a full day of work in front of me. Yeah. I mean, yeah. **Chris Romeo (17:18)**: Might as well go out early in the morning before you put a whole day's work in. **Izar Tarandach (17:23)**: This is a FedRAMP compliant podcast. We don't talk about the US, we talk about superintelligence. **Chris Romeo (17:29)**: We're not going to get our federal grant money, which is why we were doing this podcast the whole time for that $995 grant money per year. **Izar Tarandach (17:40)**: Superintelligence, la la la la. Yeah. **Chris Romeo (17:44)**: No. That was actually a nice move. That was like your superhero pose. I prefer the One where you hit the ground like Captain America. Oh, here comes Hulk. I could see Izar as— Izar would be a funny Hulk. Cause he doesn't really— I don't— you're not a super angry guy. **Izar Tarandach (18:04)**: Hulk sort of bashes. Hulk not invested enough to bash. **Chris Romeo (18:11)**: That's your— that's definitely your superhero. All right. So let's talk about formal verification. Let's see how that plays in. Let's see if we could, let's see if we can tie that into this conversation. Wait, wait. And boy, what are you getting academic here? What are we doing? **Izar Tarandach (18:28)**: I'm getting formal. **Chris Romeo (18:29)**: Okay. I thought you might've had a tweed jacket with those little like elbow things, whatever. Actually, **Izar Tarandach (18:35)**: you **Matt Coles (18:35)**: know, **Chris Romeo (18:35)**: if, if, **Matt Coles (18:36)**: if you have a, if you have a pipe and, and a foot of rope. **Chris Romeo (18:39)**: No, we don't allow pipes to be part of this podcast because you meant like a pro— oh. **Izar Tarandach (18:45)**: Not **Matt Coles (18:45)**: that **Izar Tarandach (18:45)**: pipe. **Chris Romeo (18:46)**: Oh, I thought you were talking— I gotcha. Okay. **Izar Tarandach (18:49)**: I thought if I put on a tuxedo, people are going to, to think that I'm going 007, not the formal. **Chris Romeo (18:55)**: 007. I like how you use that. **Izar Tarandach (18:57)**: Yeah. **Chris Romeo (18:58)**: It's not double O seven, it's zero zero seven. Secret agent, man. **Izar Tarandach (19:02)**: Right. You people call it double seven. Yeah. Sorry. **Chris Romeo (19:05)**: Well, Ian Fleming, the guy who **Izar Tarandach (19:07)**: wrote the **Chris Romeo (19:08)**: book, **Izar Tarandach (19:08)**: because it's too boring to say twice the same word, zero zero. It has to be something like Double zero. Yeah, sure. **Chris Romeo (19:15)**: Well, he is a super agent. Come on. **Izar Tarandach (19:17)**: Americans. Oh wait, I'm American too. **Chris Romeo (19:19)**: Yeah. **Izar Tarandach (19:20)**: All right. **Chris Romeo (19:21)**: So formal verification. So I remember this and we talked about this about 2 years ago on the previous podcast called the Security Table. The formal verification came up and, but now we've got superintelligence and what if we take superintelligence and we point it at a codebase and say, formally verify this thing, is that even, is it more possible? Start there. Is it more possible today than it was 2 years ago? **Izar Tarandach (19:53)**: Well, it's good to say formally no, but the thing that I think is gonna come, and this comes from some other stuff that I've been doing with AI, it's going to create something so very convoluted, so very jargon-loaded, so very pseudo-mathematical that most people won't be able to actually look at it and formally say, oh yeah, this is right. **Chris Romeo (20:20)**: So its own programming language, is that what you're— or just its own communication? **Izar Tarandach (20:24)**: No, no, it's going to come up with like a bunch of gobbledygook saying according to this and that, and if you call this an invariant and this idempotent and that's the other thing, it's, it's, it's, it's it's hard. **Chris Romeo (20:39)**: But isn't formal verification have to have some component of simplicity? Isn't that what makes something formally verifiable? At **Matt Coles (20:49)**: least in the historical sense, you need to make— the proofs get so complex that you have to start with a small thing first. What do you want to verify? Right? So you want to verify correctness, completeness. You want to verify some property. And so if you don't bound that, that proof is going to get very large. The number of variants, right? The number of variables, the things that can change will basically make the complexity of this formula, of this algorithm explode, right? So can you prove, you can prove certain things. Pretty well if you bound it pretty well, and then it becomes a lot easier to verify. **Chris Romeo (21:41)**: Right. Okay. Now we live in a world where we have LLMs that can do hard things on our behalf. So Ezar's, Ezar's objection is that they're gonna make it, they're gonna, they're gonna document it in such a way that we can't even prove or understand that it's **Izar Tarandach (22:02)**: correct. What Matt so aptly put that I failed to is that the proof can end up being more complex than the thing that's being proven. And I do not think, my personal, do not think that I trust the output of an LLM enough to look at it and say, well, this looks like it makes sense. Must be right. **Chris Romeo (22:25)**: What would you need to see to build that trust? **Izar Tarandach (22:29)**: I would not have anything today that would build that trust to 100%. I think that Matt, of course, is right when he says you have to start small and you have to start with little things. But then my, my, my next question is, how practical is this for the everyday system that is built? To apply. So are we talking, are we proving algorithms? Are we proving implementations? Are we proving coverage? Are we proving what? **Chris Romeo (23:01)**: Or is it just critical pieces? Well, actually, because there's, we could make a short list of critical pieces of the system, payment processing, authentication, authorization policy. **Matt Coles (23:13)**: That's too big, right? You wanna prove, you need to prove correctness. So first off, you're proving correctness, right? Correctness implies there are no flaws. So does it do what you need it to do correctly and not do anything else, right? Security issues are side effects. **Izar Tarandach (23:35)**: Yes, but I'm going to throw it out there that the security value that you could get from a formal proof, at least to the extent that I understand it, that could be completely wrong. Is going to be so, not small, but focused on the piece of code that you're trying to prove something about, and leave so much of the scaffolding around that code, that at the end of the day, from a security point of view, it's going to be immaterial. So you can prove that the crypto bits of OpenSSL are perfectly done. But that proof is not going to say anything about the verification of authentication up to the end. The use of nobody, nobody used 4 for a prime for the certificate or something **Chris Romeo (24:35)**: like **Matt Coles (24:35)**: that. That's a simple proof though. It **Chris Romeo (24:37)**: sounds like that happened. It sounds like you're describing something that really happened. **Izar Tarandach (24:41)**: But my point is that the, you know, I'm just having a horrible déjà vu here of going back to calculus classes and I had very special calculus experiences and see a proof of a theorem on the board and being unable to, from that proof, think, okay, where does that fit in the world? So that's proven, now what? And it's difficult for me to understand or to, or to imagine what would be the formal proof of no security issues. I can understand the formal proof of this algorithm is valid for something. This algorithm does what it's supposed to do and nothing else. But it's hard for me to imagine how the, the security of something can be formally proven. When the number of variables and the number of external dependencies, and I'm not talking about libraries and that bunch of stuff, talking about logical dependencies, could be so much bigger than the code that's actually in the binary. **Matt Coles (25:50)**: Agreed. And that's, and that goes back to formal verification. Proof is for correctness of function. And we should really be, we should be careful making that a statement that if we prove a function is correct, that the system is secure. The formal proof, the formal verification enables us to know if a piece, if a particular piece of code that does a certain thing is free of flaws, which contributes or should contribute to the overall security of the, of the thing in which it lives. So I don't know if you could take a full software application and formally verify it in a reasonable cost or time. Even with LLMs, but you could verify its pieces of its functionality, file reading, file handling, user input, maybe authentication might be not, might be small enough. Right. So certain methods you could probably verify that are, that are flaw-free. Now the integration, we've talked about this before, I think about its building blocks, right? So if I, if I verify Feature A and Feature B, when I now add A and B to a broader system, not all of those verifications are gonna, not all those, those, not all of those results are going to be valid because now I've integrated them together and changed the posture. **Izar Tarandach (27:16)**: So in other words, if they create new **Matt Coles (27:19)**: paths that have to be verified, **Izar Tarandach (27:21)**: if we were able to take all the security notable pieces of a system, Put all of them in a single library and then use some mechanism to prove that that library by itself is correct. And from there, assume that it's secure. I would say that that's a lot of tokens wasted because the moment that you start calling those functions from different parts of the system, that you probably cannot approve the same proof. The way that you apply those proven trustable pieces may be untrusted and probably will be untrusted. **Matt Coles (27:57)**: Yeah. So the, the article that we were referring to here actually talks about this, right? So it talks about verifying Cellphore, right? So Cellphore is a microkernel. Let me go find it here. I lost it. Where, so it's a security microkernel, right? And why can I not find it? Just looking at it, hit it when I lose track of things. So they did some formal verification of Solve-4 and— what? Sorry. I was going to quote something, but I can't find it anymore. Probably because I resized my page. Sorry. Talking out loud here. Talking to myself. **Chris Romeo (28:38)**: We can— **Izar Tarandach (28:39)**: oh, there's more than memory safety. **Matt Coles (28:41)**: Yeah, I know there's some tool I could use. Yeah. Search, Ctrl+F worked fine. So they used, they tried to verify Cellphore, right? So it's like microkernel. It took 20 person years to formally verify it. Now, does that mean that— **Izar Tarandach (29:03)**: But wait, where is it that they verified? What does verification mean in this case? **Matt Coles (29:10)**: What they, what they verified, they actually published their formal verification paper. They did machine-checked formal verification of Cell4, which is a microkernel. They verified its C implementation, IPC communications, and the kernel. **Izar Tarandach (29:33)**: Okay. That's what they verified. **Chris Romeo (29:34)**: Simplest case. **Izar Tarandach (29:35)**: But what was verified? **Chris Romeo (29:36)**: But they use, so what they, they verified using fuzz tests. **Matt Coles (29:41)**: They verified all possible code paths. They verified all possible code paths. **Chris Romeo (29:44)**: Using fuzz tests as the input. They took the existing fuzz tests and turned those into proofs. So it's a very, it's a, it's, it's not a full, I wouldn't say this is full formal verification of that software. It was more focused on file processing. **Matt Coles (30:00)**: It wasn't a mathematical verification, I guess. It was a real-world test verification. Right. So verification can mean different things, right? So they used, they use code path analysis. It's, I'm just summarizing and hopefully I get it right. That they use code path analysis to verify that all of the functions did what they were expected to do and nothing else. **Chris Romeo (30:25)**: And found a whole boatload of bugs along the way. **Matt Coles (30:28)**: Found a whole boatload of bugs. And this is, Sulfur is used, it seems in Well, various places, like, uh, is it in the Airbus? I think they're implying. So it's used in very specific ways that where you need high assurance. **Izar Tarandach (30:47)**: Yeah. The, the, there is a line here on the conclusion that's bugging me somehow. The trajectory is clear. Formal verification, blah, blah, blah, blah, blah, blah, will soon be as practical as fuzzing. Is today for almost all production software. When did fuzzing become practical that I missed the memo? **Chris Romeo (31:09)**: Well, you don't fuzz all your stuff? I don't either. **Izar Tarandach (31:14)**: I barely fuzz my hair in the morning. **Matt Coles (31:18)**: So, yeah, I mean, fuzzing is practical, but it's not necessarily economical. **Izar Tarandach (31:25)**: So fuzzing as an activity is practical., but we fall always back in the same black hole. You fuzzed. It depends on, it **Chris Romeo (31:34)**: depends **Izar Tarandach (31:34)**: on where you're building. What if the next byte? No, no. What if the next byte is the one that, that, that would trigger the, the condition? **Chris Romeo (31:40)**: Well, that's why you generate tens of thousands of mutations. **Izar Tarandach (31:43)**: And what if the next one was the one? **Matt Coles (31:46)**: Do you stop? **Chris Romeo (31:47)**: Formal verification is you create all of the possible mutations that could occur, **Izar Tarandach (31:52)**: which is why **Matt Coles (31:52)**: you have to bound the problem, **Chris Romeo (31:53)**: which is why you have to bound the problem. **Matt Coles (31:54)**: Cause otherwise **Chris Romeo (31:55)**: it's, I'm, I'm way out of my league. You have to. **Izar Tarandach (31:58)**: Now, the article also offered limitations, which is great, right? They're saying, hey, there's some stuff in here that in practice, formal verification can sometimes prove less about the security of the code than we would like. To me, the words, the key words here, in practice. Formal verification is something that is wonderful, that is great. And we knew that before LLMs. In the blackboard. As soon as you jump from the blackboard to the real world, all kinds of strange limitations start creeping up. And the fact that now we have some logical engine that does the formalization much faster doesn't seem to be adding much to the, uh, you could call this a forward-looking article, but at the end of the day, we are in the same place that we were before. We can generate a lot of stuff, but then we look at it and you say, now what? **Matt Coles (32:54)**: Now it is interesting. We are talking about LLMs, which are non-deterministic. And so what they're writing is a set of, basically a set of requirements, right? They're, they're setting a bunch of, uh, defining a bunch of rules that need to be checked. **Izar Tarandach (33:14)**: Those would be goals, right? **Matt Coles (33:16)**: Those would be goals. The AI writes the proof based on the data that it gets. It says, this is my code, this is my results. **Chris Romeo (33:25)**: But it's not doing it in a determined or a, it's not, the model's not doing it from what I'm reading here. They, they turned it over to this RockCube software, which then ran every po— and they did run every possible input. I was only joking before when I said that, that you have to run every possible. That's how they got to run every, that's how they're calling it. They're, but they're calling this formal verification because they're saying we ran every possible thing that could happen for input. And then this is the pile of bugs. **Izar Tarandach (34:00)**: Let me guess, this, this RockQ or something, that's basically a formal logic engine. That gets rules, transformation rules saying if this, then that, and that is true. So we are losing the non-determinism in the use of a formal language. **Matt Coles (34:19)**: Right. So interestingly, let's, let's, let's, let's take a look at the specifics on this one. Over the span of a few weeks, Claude successfully patched bugs it found and then proved that there are no crashes on any input up to 64 megs in size for 239 entry points across 123 different OS fuzz libraries. The typical proof was 600,000 lines of code providing security guarantees on binaries with a length, median length of 18,000 RISC-V instructions. **Izar Tarandach (34:56)**: So it's doing what, just memory checking? **Matt Coles (34:59)**: It was memory checking of small functions, right? I mean, 18,000 RISC-V instructions sounds pretty small, right? So they took a defined thing, they took a very constrained thing and proved that all possible inputs are correct. **Izar Tarandach (35:23)**: Up to the length of 64 megabytes. So, A, we don't know anything about 64. Plus 1, **Matt Coles (35:30)**: right? **Izar Tarandach (35:30)**: 6 megabytes plus 1 byte. **Chris Romeo (35:32)**: Mm-hmm. **Izar Tarandach (35:34)**: And so **Matt Coles (35:34)**: they claim it actually, we don't know if 0 is part, we don't know if 0 is included in that, by the way. We, we only know it's, we don't, don't know the full limits of **Izar Tarandach (35:43)**: it. But then comes the question. Now what? **Chris Romeo (35:47)**: Now they have a whole bunch of bug fixes for the problems that were found. **Izar Tarandach (35:51)**: For those small functions, for, for those small text functions. **Matt Coles (35:54)**: Right. So now you know that those functions have no flaws. **Izar Tarandach (35:57)**: And when 9 AM clicks and I turn this, I turn to my work desk, uh, laptop, how's my life better? **Matt Coles (36:11)**: Well, if you're using RISC-V, you're marginally better because the functions you're using are now proven to be correct. **Izar Tarandach (36:18)**: But yeah, so those three guys would be very, very happy. **Chris Romeo (36:23)**: But they, this is only in regards to like file processing, which is, I guess, what the libraries are doing. **Matt Coles (36:32)**: Yeah. **Izar Tarandach (36:32)**: Yeah. Well, but, but, but on the point of view of the memory corruption issues, doesn't say anything about that. **Chris Romeo (36:39)**: Which are common things that happen in file processing libraries, right? It's easy to have memory corruption when you do that. **Izar Tarandach (36:47)**: Yes, but. Yes, but. Type-safe and memory-safe languages and compilers have been a thing for a while. Not that they don't have bugs themselves, but there are other ways of dealing with this stuff that do not depend on formal logics of blocks of up to 64 megabytes. **Chris Romeo (37:09)**: So I'm getting that these are just a formal verification hater. **Izar Tarandach (37:13)**: No, I'm not. No, I'm not. I'm thinking that. That's a great way to go, but formal verification of the things that we have today, perhaps before they are heralded as yet another great revolution, they should be practical. And this does not seem to be practical to me. On the other hand, working off of formally provable programming languages might bring better results over the horizon than this. **Matt Coles (37:43)**: So honestly, I'm the issue I think I have with all of this, the automation to prove correctness is awesome. **Izar Tarandach (37:51)**: Yeah. **Matt Coles (37:52)**: But, but where I have a, where I have a, I'm curious about is using an LLM to fix the bugs that are found. **Izar Tarandach (37:59)**: Are you introducing more? **Matt Coles (38:01)**: Well, that's, that's one. How do you verify that the bugs are actually getting fixed and not introducing new side effects? **Chris Romeo (38:07)**: In this case. The model, they're, they're, they're creating these RockQ proof language files, **Matt Coles (38:19)**: right? **Chris Romeo (38:19)**: Which are then the source of truth. So it's a deterministic, **Matt Coles (38:23)**: it, it's test-driven development. **Izar Tarandach (38:25)**: Yeah. **Matt Coles (38:26)**: But, but it's, how do we know that what Claude is writing is free of defects? **Chris Romeo (38:34)**: What it, what is, because when Claude writes something, writing what? **Izar Tarandach (38:36)**: All the tests are green. It might be 100%, but it's library **Chris Romeo (38:40)**: code. The theorem, the proof language code, **Matt Coles (38:44)**: all **Chris Romeo (38:44)**: of it, **Matt Coles (38:45)**: right? They're writing the code, they're writing the patch, and they're writing the verification of that patch. **Izar Tarandach (38:51)**: We talked about earlier. **Chris Romeo (38:52)**: Yeah, it is, it is test-driven. It's tests are what are driving your ability to explain. **Matt Coles (38:57)**: Should the plot be writing its own proof? **Chris Romeo (38:59)**: No, probably not. Back to the first, the thing I said earlier. **Matt Coles (39:03)**: Right. **Chris Romeo (39:04)**: You need to, we need to live in a multi-frontier model world where if you have one do something, you should have the other one either check it or do the other thing. Like don't have Claude write tests for code that it wrote. Have Codex write tests for the code that Claude wrote and, and code review, have one review the other. And I've found some really interesting things when you have one frontier model review another frontier model's code. **Izar Tarandach (39:39)**: So you're telling me that compounded mistrust equals trust? **Chris Romeo (39:44)**: Compounded mistrust equals trust. **Matt Coles (39:46)**: 3 lefts always make a right, right? **Chris Romeo (39:48)**: It's the best that we can do right now. **Izar Tarandach (39:52)**: Do you think that video from last week of the two AI is interviewing each other and they couldn't get out of it because they kept saying bye-bye, bye-bye, bye-bye, bye-bye. Do you think that they were using the same model or two different models? **Chris Romeo (40:07)**: Probably using the same model. That's why they got caught. **Izar Tarandach (40:10)**: I say it doesn't matter. At the end of the day, they got into a loop. **Chris Romeo (40:14)**: Loops are certainly possible. **Izar Tarandach (40:17)**: So that, that, that's the thing. If we don't trust A, we don't trust B, we don't trust C. Putting A, B, and C in a pipeline and having them mix and match results does not give me more trust. **Chris Romeo (40:30)**: The alternative is to just live under a rock and not use advanced technology. **Izar Tarandach (40:36)**: Depending where the rock is. **Chris Romeo (40:39)**: This is, this, but this is the, I mean, the, the bigger issue that you're describing. I've heard other, I've heard this play out in multiple different ways. But it's the, the, the, it's the anti-AI crowd. So I'm not saying you're, I'm not saying you're a part of that, but that's, but that argument is going in that direction. Like there are some people that are, that are arguing against the use of AI still to this day. **Matt Coles (41:05)**: And **Chris Romeo (41:06)**: it's like, we just did a, we did an AppSec podcast with Brooke and Brooke brilliantly just described this, like either get on the boat with us or the ship has already sailed. Like if you're not, if you're saying, well, this isn't gonna change the world, this isn't gonna change how we build stuff. **Izar Tarandach (41:25)**: Chris, Chris, look, look, I use AI every day, day in, day out. Okay. I'm even over the bump of feeling guilty about using AI to code, but there's a difference between being the guy in the front of the Titanic saying I'm the king of the world, And being the violinist playing until the water gets to your waist, right? **Chris Romeo (41:50)**: Mm-hmm. **Izar Tarandach (41:51)**: What I'm saying is, sure, let's use it, but let's not think that it's the solution for everything under the sun because it's not. Now let's use it with enough mistrust. **Chris Romeo (42:01)**: But you trust it enough to use it every day. **Izar Tarandach (42:04)**: No, I'm, I'm saying let's use it with enough mistrust so that it forces us to keep some modicum of cognitive capability to make sure that what we're getting is actually what we want to get out of it. **Chris Romeo (42:18)**: Let me ask, let me just make this really spicy. How many lines of code did AI generate for you last week, roughly? **Izar Tarandach (42:28)**: I wish I knew because I didn't go and read all the code. **Chris Romeo (42:33)**: How many, how many, good, this is, I feel like a lawyer on one of those shows because you're walking right into my, you're walking right into my trap here. I am, I am, I see where I'm, I see where I'm going. How many How many lines of code then did you review yourself to enhance the trust that you had in the output that was coming from the coding agent? **Izar Tarandach (42:51)**: Less than 100 of what got produced, probably, because I don't know how much got produced. **Chris Romeo (42:57)**: Matt, your honor, I rest my case. Hit the gavel. **Izar Tarandach (43:00)**: So, so— No, I'm going to— no, no, no. Now I'm going to get to take you on another tangent. Not one single line of the code that I had produced. Was critical in any way, shape, or form. This was all stuff that I was willing to throw away. **Chris Romeo (43:15)**: So it was all prototyping. **Izar Tarandach (43:17)**: Because what it did was shape up something that I had in my head to give me the possibility of seeing that I was going somewhere valid with that. Now, the moment that that thing becomes a product, the moment that that thing goes somewhere critical, the moment that people depend on that thing, the way that I relate to that code will be very different. Because that's what I've been asking from my developers for the past 30 years. **Matt Coles (43:40)**: That's the, that's the point. Trust. Trust. How do **Izar Tarandach (43:46)**: you, that's the point. **Matt Coles (43:47)**: Where do you, where do you, how, how do you get, how do you establish trust in the code that gets written? And you would do it whether it's a developer or AI. AI is just a developer. **Chris Romeo (44:00)**: Formal verification, Matt. Of course. **Matt Coles (44:02)**: Of course. **Chris Romeo (44:03)**: Full circle. **Matt Coles (44:04)**: There we go. **Chris Romeo (44:05)**: We came all the way back around. **Izar Tarandach (44:07)**: But actually, before we go to the formal verification, I would stop on what we already have. We use the deterministic tools that we already have. **Matt Coles (44:14)**: Right. **Izar Tarandach (44:15)**: We, of course, definitely, completely, always use threat modeling. **Matt Coles (44:20)**: Right. **Izar Tarandach (44:21)**: Because that's the point where you look at that mass of code that got created and you decide there's enough critical stuff in here to rewrite or to completely go and read. **Matt Coles (44:30)**: Right. And by the way— **Izar Tarandach (44:32)**: These are the big flaws that might happen in the way, and this is how I'm going to stop them from happening. **Matt Coles (44:37)**: And let's bring back another topic that we just talked about. You have this data to information to knowledge to wisdom stack, right? Use the tools to find data, then turn it into information and knowledge and wisdom. And you pass all that information back, whether you're training your developers You have security champions, you're training them on security techniques or on good code constructs or guardrails and paved roads, right? The, whether you're doing that to a human developer or a team of agents and subagents, it's that feedback loop. Nothing changes, nothing changes, right? It's just another set of hands. **Izar Tarandach (45:22)**: Uh, one thing changes and it's, yeah, I think it's very important. Sorry, what's the term of the Zeitgeist? It's load-bearing. **Matt Coles (45:29)**: Oh God, don't do that. **Chris Romeo (45:31)**: It's load-bearing. **Matt Coles (45:33)**: It's load-bearing. I don't know who, where that was introduced. Somebody trained their models on bridge construction or something. And that's where that's— **Izar Tarandach (45:40)**: So when we're training people, you are able to an extent to say, please don't do this and walk away with the hope and some trust that they won't do that. Apply the same thing to an LLM and it's a suggestion that may or may not be taken into consideration. **Matt Coles (46:02)**: It's a suggestion unless you do other things, but it's the same thing with a, with a human, right? A human could ignore the suggestion. **Chris Romeo (46:10)**: Humans are, humans are opportunistic. **Izar Tarandach (46:12)**: You can tell **Chris Romeo (46:12)**: a human, **Izar Tarandach (46:14)**: you can tell a human, if you don't follow this code standard, you're fired. **Matt Coles (46:18)**: And why can't you do the same with an AI? **Izar Tarandach (46:20)**: Because the AI doesn't care. It acts as if it does, but it doesn't. **Chris Romeo (46:25)**: Yeah, but if that, if that was true, we would have solved our problems a long time ago. Look, if, if we could have said, just, if you don't follow this, but as people, if we, if we were able to, to go to the engineering team and say, here's our secure coding standard, it's, I know it's 300 pages. If you don't follow this, you're fired. If it was that simple, we could have done it 20 years ago. **Izar Tarandach (46:46)**: We can't do that because as some Altman said, Nobody saw the, the, the, the, the curve coming, right? The, the, the intuition of nobody took security seriously, right? **Chris Romeo (47:00)**: Fabrication or something. I don't know what it's called. **Matt Coles (47:02)**: If the tool, if we hadn't, didn't have AI, you would've had better and better tooling, right? **Izar Tarandach (47:07)**: Yes. **Matt Coles (47:08)**: And we would've potentially still hit this curve over time. **Izar Tarandach (47:12)**: Yes. Potentially over time. **Matt Coles (47:14)**: But we just hit it so fast, right? This curve. **Izar Tarandach (47:16)**: Yes. **Matt Coles (47:17)**: On time went vertical. **Izar Tarandach (47:19)**: People just saw this all of a sudden. It's not that we hit it so fast. People just saw it all of a sudden. We've been telling people at a less steep angle for the past, I don't know how many years, but now all of a sudden it's thrown in their faces. **Matt Coles (47:36)**: By the way, **Izar Tarandach (47:38)**: by the way, **Matt Coles (47:38)**: by the way, you can fire your agent. It's called creating a new session. And this goes back to the throw it away and start from scratch. **Izar Tarandach (47:46)**: Right. But you can't just fire your **Chris Romeo (47:49)**: team. Okay. When **Izar Tarandach (47:50)**: you get mad at **Chris Romeo (47:50)**: their output, **Matt Coles (47:51)**: I can **Izar Tarandach (47:51)**: delete all I want. **Chris Romeo (47:53)**: No, I, I keep mine. I'm like, I don't care if you're at the context window. You and I are friends, **Izar Tarandach (47:58)**: but they **Matt Coles (48:00)**: copy **Izar Tarandach (48:00)**: that. That's clear. That's trust. But my point is that, um, no, that's **Chris Romeo (48:06)**: not trust. That's odd. You can say it. **Matt Coles (48:09)**: That's misplaced trust right there. **Izar Tarandach (48:11)**: My point is that LLMs are not compilers, and people keep relating to them as if. I'm going to say, do no mistakes, make no mistakes, and that's going to be my next pragma, and the compiler is going to always take that into consideration and not create these constructs, because the pragma is in there. LLMs are not compilers. Start talking to them or feeling them as they are. **Matt Coles (48:33)**: Compilers are deterministic. **Izar Tarandach (48:35)**: Exactly. **Matt Coles (48:36)**: They're rule-based. **Izar Tarandach (48:37)**: And if I had the mic, I would just drop it now, but I don't because it's expensive. **Chris Romeo (48:41)**: With that, we'll wrap up this episode because Izar wanted to have a mic drop, but I'm going to talk about, I'm going to talk over it so that the mic drop gets kind of run out to the end. **Izar Tarandach (48:51)**: Damn it, Carl. **Chris Romeo (48:52)**: Carl will be making an appearance soon on the AI Security Table. He's our correspondent. He's in the field. It's in the field, I should say. **Matt Coles (49:02)**: Somewhere. **Chris Romeo (49:03)**: We could actually send Carl into the CPU for an update. It's Carl coming to us from the CPU. Have the fan blowing in the background like he's a weather reporter. **Matt Coles (49:12)**: Wait, wait, wait. Not the CPU. He's not. **Chris Romeo (49:17)**: The GPU. **Matt Coles (49:18)**: The **Chris Romeo (49:18)**: GPU. Well, he can move around inside the computer components. Come on. So it'd be like an after-school special. He's just a bill on Capitol Hill. It'll be that kind of a style. **Matt Coles (49:31)**: He's writing the GPU. He's writing the NPU. **Chris Romeo (49:35)**: You gotta be a certain age to understand. I was, I'm just a bill on Capitol Hill. **Matt Coles (49:41)**: Just a Carl on my computer. There's no, it's, it doesn't roll off the tongue as well. **Chris Romeo (49:47)**: No. All right, folks. Thanks for listening to another episode of the AI Security Table. Thanks for joining us at the AI Security Table. Subscribe, rate, review, and follow wherever you listen. New episodes every week. AI Security on the Table.