AI:AM — AI-Generated Code, Formal Verification, and Agent Security · October 12, 2026

I still firmly believe that writing code is a dead art in 2 years tops. AI is fully driving interactive theorem provers now.

You can tell your agent now that you have the code, write down the specification in Lean and prove the code correct and let it deal with it.

We're going to have mass-manufactured software that if it doesn't fit the mold of it's been specified, it has the correct API boundaries, it has formal verification attached to it, it doesn't fit in the package repository. And we did that by actually taking the C code that existed and porting it to Rust. using an LLM and then using differential fuzzing to ensure that the ported code to Rust was correct. And any divergences there would have been a source of a potential bug in the original C code. And we found a bug at that stage. And then when we went to take the Rust code and also verify the correctness of the Rust code, we found a bug at that stage as well. Like I was saying earlier, the maintainers explicitly told us we're not interested in maintaining a Lean model. We're not interested in maintaining a Rust codebase that's separate. We've got our C code and we know it very well and we want to keep maintaining that because it's what's working in industry on all the devices around the planet right now.

Because of AI, all the code that will be deployed that is not formally verified, or let's not say formally verified, that is hackable, will be hacked because it can, it can be hacked easily with AI these days, right? So this kid in Bangladesh will just hack NASA if they want to, if they can. Okay, so that's why it will be irresponsible for enterprises to deploy code that is not bulletproof, formal-based.

And typically what has ended up happening is that we have poorly specified, you know, poor specifications from the user or the consumer or the business, and then you have the PMs in the middle Trying to translate those, uh, poor and vague specifications into things that the developers can actually implement.

First, the news. Claude locks Nathan out of his own agent console, which raises who holds authority when an AI fallback fails and whether China should face AI's risks first. Then Everett Hildenbrand and Grigor Rosu of Runtime Verification on what a developer still has to do when AI writes the code and attempts the proof. After that, the hosts on why formal verification is not alignment and why planes still carry pilots, a review of the YPO conference, and a close on AI volunteers proving faster integer multiplication.

What has happened in AI over the weekend?

Some reason Claude decided it was in my best interest to rotate the passwords that are used in my agent console. I'm trying to depersonalize some of the custom software that I've written so I can put it out onto a GitHub repo and just share it with other people. And somewhere along the line, it decided it needed to rotate passwords to, you know, do this in a secure way. So it's probably right. I'm locked out of my own agent console. I don't know the password. The password was created by Claude, saved somewhere. It can change the password on my Access to itself wasn't actively trying to screw me over, so it just readily told me where to find the password and I was back in business in 2 seconds. But you can see, like, if the intent ever is bad on the part of Claude, like, it can already lock me outta my own shit. And so I've been thinking quite a bit about kind of how people need to maintain, first of all, they need to understand this architecture and then they need to be mindful of like, what are the levers that I am giving AI control over that I better also retain pretty clear and ready control over in case it ever really becomes needed.

So it strikes me that a lot of people actually tend to think of technology as ready to fail. My first job was working in an airline. I've seen internally every airline, every airport is a cascading system of what to do when things break down. From the check-in counters to the reservation systems to the bookings, et cetera, et cetera, et cetera, et cetera. And so much so that you could basically revert to a pen and paper system overnight if you needed to. And how that happens is actually there's a set of contracts underlying all international travel called IATA guidelines. So for example, I could buy a United Airlines ticket, and I could travel on like JAL. And the person at the front desk has the ability and has the power in an emergency just to say, go. You can do it off a piece of paper. The accounting stuff can take months to happen after, but there's a set of predetermined contractual terms between the airlines, which they've agreed to over the decades, which will basically determine how the cash flows flow. All of the systems in between are all about really allocating risk, allocating liability, and allocating, like, who pays for it.

But I do think we're going to need that kind of stuff for AI. And like smaller, you know, medium-sized businesses that aren't used to thinking about, like, operational redundancy type questions, it's going to be a fresh challenge. And one that is going to be very easy to neglect, I think, in a lot of cases, but I wouldn't be afraid to use AIs to map out and, you know, contingency plan and set up my, my protocols.

Industry has asked Washington to carry its risk before. Since 1957, the Price-Anderson Act has capped nuclear operators' liability, with the federal government backstopping claims beyond it. Now AI companies are making a similar ask. Who carries the risk this time?

Some of what the AI companies are doing is trying to shift a bunch of their risks down to the federal government to have them be federally insured by the government as a backstop rather than liability product insurance at the top end. Because they're saying, look, we're running ahead so fast, we don't have time to create the product liability insurance and to delay that. We can if you want to, but then we'll lose to China. So if we're going to run this fast, Then you should give us the backstop on the liability so that we don't have to delay on the product liability side on the front end. I've only heard this recently in the last few weeks. Some people are saying, like, okay, if that's the deal, it was to China, there's all of this liability and there's all these risks, then if they go ahead, they're going to hit the risks first.

I think this has been sort of a healthy turn on kind of calling the China bluff. And I do think they are going to probably be more Cautious about a lot of this stuff than we are in the end.

This episode asks what a developer still has to do when AI writes the code and attempts the proof. The founder and the CEO of Runtime Verification have spent 16 years selling exactly that assurance. And this month, their method found a silent defect in the Linux kernel.

So, our first guests for this morning are, uh, Grigori Rosu and Everett Hildenbrandt. Grigori is a computer science professor at the University of Illinois at Urbana-Champaign and the founder of Runtime Verification, a company that audits software and develops tools for checking its behavior mathematically. He's also the founder and CEO of Intent Computing, where his work concerns generating software together with precise requirements and machine-checkable proofs. Everett Hildenbrand is the CEO of Runtime Verification. a company that audits critical software and builds tools for checking it with mathematical methods. Its engineers work on a precise question: does a program meet a stated requirement for every input covered by the analysis, rather than just the examples someone thought to test? Your team found Linux could silently install a different user identity mapping from the one requested. Your October report says the discovery came while writing the specification, before the proof found anything. Talk us through how your team went from writing the specification to discovering the wrong mapping.

So, well, we, you know, we have been doing formal verification for a long time, and so I think it benefits us to start and just describe what formal verification is. You know, it's this idea of mathematically modeling the intent of a specification, which is, you know, someone's usually human-written list of requirements and behaviors. that you want a system to adhere to, and then checking that the implementation actually meets that intent. You don't wanna build the bridge once and then say, let's send some cars over it and see if it works, and then have it break and then be like, okay, I guess we need to beef up the supports underneath the bridge. You wanna build it once and have it work every time, right? And so when engineers are building bridges, they do formal verification. They make a specification of the loads and the wind stress that the bridge needs to be able to handle. And then they design the bridge to handle that, and then they do formal verification using math to check that the bridge will be able to handle that. And so the idea of formal verification applied to software is unique because software is so much more complicated than bridges that it is, you know, it's intractable to do that. And so instead, with software, we do take this iterate and test approach. The other reason is because iterating with software is so much cheaper than iterating with bridges. But software is getting to the point where failures in software are as expensive and devastating as failures in bridges. And so it's important that we bring formal verification into this. And so this recent work we've been doing on the Linux kernel, what we've been doing is looking at the parts of the Linux kernel that are

sensitive to failure. And so that means for us, parts of the Linux kernel that may seem simple, but are accepting untrusted user input.

And developers hate specs, right? And typically what has ended up happening is that we have poorly specified, poor specifications from the user or the consumer or the business. And then you have the PMs in the middle trying to translate those poor and vague specifications into things that the developers can actually implement. The developers themselves often do not want to deal with the specs. They're like, look, I will take the spec and I will implement it, but it's up to you to come up with, you know, good specs. And if your specs are poorly specified, that's your problem. Uh, the PMs are supposed to fix it. So, you know, you have this very famous XKCD cartoon of like, you know, this entire structure and there's one small piece which is being maintained by some guy, uh, who has been doing it for like 20 years. And that's what all All of the internet rests on Topper, right? So I feel like a lot of the software that we do use right now is lots of libraries, and people are just adding in npm from here, et cetera, et cetera. And they're just accumulating these structures of software where they don't really have visibility on the correctness of any of those pieces. And they're just focused on their specific thing that they're trying to do.

We have companies that offer, for example, private npm registries where they check, you know, every piece for public CVEs and stuff like that. I firmly believe within a couple of years at most, part of that checking process will be coming with, does it have a formal specification?

Where are we in terms of how much sort of insight or eureka kind of moments are needed to get those specifications right versus like how much can be the subject of an LLM grind?

The general high-level bird's-eye view between specs and code is that specs address the question, what? What do you want your system to do? While the code addresses the question, how? How do you want that to be implemented? Then mathematics allows you to bridge the gap between the two, what you want to do versus how you do it. And there have been many, many, many specification languages and logics supporting them developed by computer scientists, mathematicians, and now also AI part of the game. Usually specification languages work really well for specific domains. If you pick a domain, let's say navigation software, then you can come up with a very nice specification language for that domain, because there is a clear one-to-one intuition between what you have in mind and what you see in the specification language. But of course, we want specification languages that are very general, that work with everything. So we have a framework in runtime verification that started at the University of Illinois Urbana-Champaign, where I teach programming languages and formal verification. We call it the K Framework. And you can go to kframework.org and learn more about it, which is a framework that allows you to do both, to specify both properties of systems and programming languages and programs. So it's like a universal specification language that allows you to do all of this together. But until recently, the drawback of such a universal specification language was that it can be very tedious to describe certain intents. But now, thanks to AI, this is a lot easier, much easier than it used to be. We play with some models, we train them with the K framework, and they take your intent and generate a case specification for you pretty quickly, actually, and unbelievably well. Of course, you still want to look over it, but it does it well. And when you combine that also with code, generate spec and the code together and prove them together, then it's becoming really powerful. And at least I believe that this will be the future, actually, when we generate everything together. At once, code, spec, proofs, everything. AI will generate it for us. We just verify.

It's a very gameable experience teaching code. Actually, working with interactive theorem provers is the same. It's a very gameable experience. And it's also exactly the experience that AI is taking over fully. The AI is fully driving interactive theorem provers now. And I think anything that is that gameable experience, probably AI is going to be good at doing.

Transcript. Runtime verification earns its living auditing code other people wrote. And this month, its Rust tool joined the Rust Standard Library Verification Challenge. So its CEO has a stake in the answer. How long does writing code by hand stay a job at all?

I firmly believe that writing code is a dead art in 2 years, tops. It's all going to be about writing specification and intent and making sure that— and so your package, part of your package delivery is not, uh, not just, you know, did I get it into the registry correctly, did I define the API. It's also going to be, did I provide the formal specs, did I provide the lean proofs, did I provide the actual logic that dictates how this package is supposed to behave. And I I see no reason why that will not be the case in 5 years tops. We're gonna have this intermediate period between now and then where it won't be the case, but I think gone are the days of, of what I think of as like the cowboy coder or something like that. Now is the days of mass manufactured software, you know, just like the same with like mass manufactured bread, for example. Sure. It's not exactly the loaf of bread you want. Doesn't have all the characteristics of something made in an artisanal bakery or something like that. But it slices cleanly every time and it makes the same sandwich every time when you use it on the next step in the production line. Software is going to be the same. We're not going to have artisanal software anymore. We're going to have mass-manufactured software that if it doesn't fit the mold of it's been specified, it has the correct API boundaries, it has formal verification attached to it, it doesn't fit in the package repository because it just will be too risky.

So can you maybe tell us just a little bit more about, like, the Linux example in particular is just such widely used, you know, the whole theory of like, all the eyes on this critical software will make it secure over time. You know, broadly seems to have served us pretty well. So why was this not caught previously? What was it about your approach that allowed this to rise to the top where so many Human eyes had presumably just, you know, blown right past this issue in previous reviews.

The key for us was that we had a hypothesis about what would be a good place to look for bugs. And we, you know, thought about it logically in the same way you would think about, you know, making a formal specification. And we pursued that path, basically. And that hypothesis was largely founded on, okay, where are we going to be able to get untrusted input from? Which parts of the Linux kernel probably are getting less scrutiny than other parts. And so that's why we focused on device drivers, for example, as our first approach to that. We focused on places that are kind of at the kernel and user boundary and at places that are specifically taking user input and parsing it and trying to make decisions with it. And

once we had identified a few such places, we went through and started defining, okay, what does it mean for this component to be correct? And just started writing that down. And usually when you're writing that down, you have to do a mixture of reading through old forums or old threads and reading documentation and then reading the code itself. And you're kind of teasing out what the original intent of that piece of code is in the process. And oftentimes, almost every time we ever do this, we find somewhere where the code does

something unexpected, where it diverges from the behavior that's written down in the specification or from what was stated in the forum post. Or something like that. And that's usually an indicator that there's probably a bug lurking in there. That's the specification portion. You need to do the actual verification portion, right, which is where you go and you prove that the code actually implements that behavior. So that's what we did, is we took a methodological approach where we said we're going to focus on making a specification of the correct behavior of this and then testing that the specification is correct using differential fuzzing. That was the first approach that we tried out, and then extending that to formal verification. So every, every step of the methodology that we used was designed to increase the level of confidence we had in the code incrementally. And we did that by actually taking the C code that existed and porting it to Rust using an LLM, and then using differential fuzzing to ensure that the ported code to Rust was correct, and any divergences there would have been a source of a potential bug in the original C code. And we found a bug at that stage, and then when we went to take the Rust code And also verify the correctness of the Rust code, we found a bug at that stage as well. Didn't just take an LLM and point it at the Linux kernel and say, go find us bugs, which also works, by the way. But one of the things that, you know, emerged pretty early in the use of LLM bug hunting was, you know, designing harnesses and approaches. And that exactly mimics the very human process that we've been doing for decades with software quality assurance anyway, which is to Have these methodological approaches to discovering bugs. There's techniques that have a track record for working, and we should just use those. And we should teach our agents to use those techniques as well.

How does this relate to agents, agent control? Because again, the agents are building on top of all of these layers below them. A lot of those layers are not fully verified. You have these agents running around and the entire stack is basically random pieces of architecture. You know, plastered together. How do you build from where we are to what you're going to need in order to have agents which are reliable?

We're not there yet. We have a lot of work to do. I think the key is to make people aware of the risks of incorporating software that is non-standard— non-standard meaning does not come with a specification— in your supply chain. And most enterprises already are aware of this risk, and they already have tools for mitigating against supply chain attacks. You know, this is going to be one more of the risks that they add into the, okay, how do we select vendors?

And also can be combined with risk mitigation techniques like runtime verification itself as a field. So the idea is that you can have safety specifications, not full specifications of the whole system, but safety specifications. This should not happen. And if it happens, then this should be the recovery. I want to steer the system to stay in this stability envelope or safety envelope. So what we can do, we can now with formal methods generate monitors which are provably correct for these safety specifications. You may not be able to prove the entire AI system or AI-generated system correct because it's so complex and relies on so many other pieces that are incorrect or not proved. But I can prove my monitor and the stability, the safety envelope. It's impossible to prove the weights correct. It's impossible to prove you correct. But I can have a police system around to make sure that you don't do bad things.

Linux is maintained by a hierarchy of reviewers who vet every patch by hand. And Runtime Verification's October report says its fix for the identity mapping parser went upstream as a patch, not a proof. What did it take to get those maintainers to listen?

You can't just go force people to do formal verification. They're only gonna adopt, you know, methods that bring them value. And so our first attempts at this, we approached Linux kernel maintainers and we said, hey, like, we really think that this formal verification thing has legs and that it will, you know, that it will help you guys find bugs and it'll make your software more secure and stuff. And they basically told us to go kick rocks. They're busy maintaining the Linux kernel. And so then we were like, okay, let's prove the value of this first. So we decided we're going to focus on a workflow that just delivers immediate pure value to them and doesn't ask anything of them. And all of that leads to bugs and patches, bugs and patches. And that's what's actually valuable to the Linux kernel maintainers. And now that we've submitted a few, now we're being invited. We want to learn about how you have done this process. And so really it has to be something that is integrated into the developer workflow early.

I have 2 big questions in mind at the moment. One, is just on kind of the limit of agent control in the context of ever more verified software. It's one thing to say, okay, we want to make sure that the tools and the environments that the agents are running in are not exploitable, because we've obviously seen recent examples that have captured the imagination around what can happen when they're not. But it still seems in a sort of fundamental way that there's this inherent tension where part of what I want from an agent is sort of the same thing that I want from a human employee, which is like, I want you to be able to get over the hump and solve problems that were not anticipated. I'm asking for your vision, I guess, as to how we balance this desire of Flexible problem solving versus this should never happen. Is that an inherent trade-off? Is there some way to square that circle?

You're not going to ask an agent like, hey, go build a bridge for me. We know how to build bridges, right? We have automated deterministic processes for building bridges. You might ask an agent like, hey, I need to get to the moon. And the agent's going to be like, oh, to get to the moon first, I need to build a bridge to this island where I'm going to launch rockets from or something like that. So you want the bridge building process To be foolproof. And so that's what I think of as the first value that formal verification brings us, is all the building blocks, all the components, the pieces of bread coming out of the bread factory need to be sliceable. They need to be uniform and sliceable and usable in sandwiches that the agents are going to build things out of. You know, all the agent creativity or solving problems or human creativity can come on top of foolproof things that behave how the agent expects. regardless of, you know, what it is they're trying to do. So that's, that's, I think, the most important thing to me is like we need to give these things tools that act reliably, basically.

We do not limit their creativity through formal verification. On the contrary, we give them the tools, the Lego pieces they can combine to build bigger things using their own creativity, but correctly. Think of it like this Lego piece does X and and now you have a stamp on it, which is the proof stamp that you know for sure that that will do X. Now, actually, that unleashes the imagination and the creativity of agents and humans and everybody, because we don't have to worry about that Lego piece being wrong or incorrect or cracking, crashing on, you know, on some other— we know exactly what it does. So there is room actually for both. On the contrary, they reinforce each other. And because of AI, all the code that will be deployed that is not formally verified, or let's not say formally verified, that is hackable, will be hacked. Because it can, it can be hacked easily with AI these days. So that's why it will be irresponsible for enterprises to deploy code that is not bulletproof, formally verified. And this is closer than ever to completely be done automatically.

So let's talk about the Linux project that you had in October. At the end of that project, you had some parts which were proven and some parts which were still open. You have 80 or something theorems that you verified, but there are still some parts which were unverified, highly unverifiable in that sense.

Well, they weren't unverifiable. We timeboxed the experiment and we stopped at the end of the timebox, basically. And then we moved on to the next target. So every 2 weeks, we're trying a different target out and we're refining the approach. And building it up into a tool that, um, we're hoping that other people can make use of, basically. So we're trying to make it into less of an expert-level tool and into something that anyone can deploy on their own codebase, basically.

You mean, uh, both the time and the number of tokens that you put in? As in, like, it's a 2-week period but you use 10,000 agents, or it's a 2-week period and you use like 5 agents?

Uh, the agentic usage was pretty light, I would say. It was just Claude code on a premium plan. Single instance. You know, when, when we ran into session limits, we'd give it a little more money, but we weren't giving it significantly very much money. So it really was more just the human time that we were looking at timeboxing there. And I think the key here was we were looking for ways to explore the methodologies that work for us and find ways to automate them. We are firm believers in making things deterministic whenever possible. I think that's part of the thing that is maybe holding back people on doing security analysis is that they believe everything has to be LLM-driven. But, you know, if an LLM discovers a technique that works well, turn that into a tool and run that tool every time. That's our approach.

So would that look different if the same person had access to 10 instances of Claude, or would it not because it's still bottlenecked by the person?

It probably would look a little different. I don't think that they were particularly running into the session limits. I think they could have, for example, within that existing session, had it look at 10 different subsystems of the Linux kernel and find bugs. So I think that, you know, the rate of it happening would probably increase. But then, you know, one of the biggest things that we're hearing from Linux kernel maintainers and other software maintainers is being flooded with bugs and patches is actually less useful than just not doing anything at all. And that's because they, you know, they have to vet every patch and the back and forth period of Even getting a patch into the Linux kernel involves some communication and talking to people and making sure you understand all the consequences of a given patch. You know, one of the things that we're really trying to emphasize is producing high signal-to-noise for these developers and also not flooding them, not just overwhelming them, because that leads to burnout. And ultimately, it's not an agent guarding patches, making it into the Linux kernel, it's a human.

So it sounds as though there's, there's two, there's two things there. One is There should be higher signal on the bug finding and escalation side. And 2 is we should have higher bandwidth for the maintainers to accept and verify bugs. Like, which one of those could be improved, you know, going forward? And which ones are the bottlenecks to having more formal verification?

The maintainers explicitly told us we're not interested in maintaining a Lean model, not interested in maintaining a Rust code base that's separate. We've got our C code and we know it very well and we want to keep maintaining that because it's what's working in industry on all the devices around the planet right now. And so we were like, okay, we need to design an approach to this that works within that framework basically. And so that approach was all the formal verification, all the translation, all the fuzzing, all the Rust modeling and the Lean modeling and everything we would own And we would use that as a process to distill patches we could ship upstream. And so one of our kind of pie-in-the-sky goals of this is eventually we want a Rust model of the Linux, the entire Linux kernel, a Rust version of Linux, and we want a Lean model of Linux fully separate. I think as far as increasing the, you know, the bandwidth for reviewing patches in Linux in particular, I mean, Linux is a very particular development hierarchy, you know, full of lots of humans at every node in the development hierarchy and a healthy skepticism of AI-assisted anything. And so that probably isn't going to increase significantly. So there's, there's people working on this problem, but the throw more agents at it is a non-starter for a lot of these people because they don't want to work with agents. They want to work with high signal-to-noise ratio patches submitted to that.

What would it take to formally verify and get to Lean and Rust models of Linux within 24 months? Because on some timelines, that is roughly what people on the AI safety side think—

That's going to happen. We're building tools for doing code translation and validation. So we have actually tools that are able to verify that when you take a piece of C code and you translate it to Rust, for example, and you can formally verify that the Rust code you got is behaviorally equivalent to the C code, which is different than verifying that it's correct, right? Like, we want to verify that you get Rust that is drop-in replacement, bug for bug, the original C code. And we have a tool for doing that. It uses LLMs to do the translation if you want, but it does the verification deterministically. Just tell the LLM, translate the thing to Rust and run our tool, and then you get verification that the Rust behaves the same as the original C or bugs out that you can ship back to the C developers. So I think 24 months, I think it's going to happen. You're going to have Rust models in Linux kernel at the very least. And there's already deterministic tools that can take Rust and turn it into Lean. Those need more work. We're actually contributing some work to some of those tools.

So you're running a startup, Everett, and also running for office and sitting on the board of a nonprofit. How AI-ified is your life such that you are able to juggle these things. I think this may be the first CEO running for office that I've heard of, and I'm very curious to unpack how you're juggling these balls.

Well, my entire campaign was done by Claude, basically. There's a human element to campaigns where you have to knock on doors and you have to like go to public debates. But, you know, I just basically brain dumped my entire campaign into a Claude code session, and I have a repository that maintains my website and all the materials that I put out. I have it write the first draft of all my speeches and also do my debate prep and stuff like that for me. So that's, uh, in one fist I have Claude, and then in the other fist for my company I have Claude, and then in my private life for the nonprofit, in my third fist I have Claude. Everything fits in the premium or max plan. You know, everyone is like, oh, we got to have 10,000 agents solving this problem and doing it. And maybe that works for things that are really reward hackable, But like getting elected is not reward hackable, you know, because you don't know until the, until the day of the election whether you got elected or not. And running a nonprofit is also not very reward hackable. So it's really just an assistant at that point. I don't need 10,000 agents doing the thing. The same with CEOing, like you, you know, it's a, it's a people job. So it's not very reward hackable. It's something where, you know, I use it to do the things I'm helping my employees do, but I'm not like— running the agent swarm or something like that.

A proof checker can confirm that code matches a specification. It cannot tell you whether the specification was the right one. Runtime Verification's post this month boils its advice down to getting better at specifications. So, who decides what the software is for? And how?

One thing I'll say about formal verification, I think that a lot of people miss is that it's very human. You have to ultimately decide what you want the software or the system to do, and you can have an agent decide that, of course, if the agent has some sort of intent that you want it to, to fulfill. But usually it's humans deciding what we want our software to do. We want the traffic lights to do something, and we want our airplanes to do something, and we, you know, we have some sort of idea of what the correct behavior of these systems is. And so formal verification is the very human process of writing down that intent and then ensuring that the software meets it. Start from your intent and you try to figure out how do I get the machine to do this intent. That's all the wizardry gobbledygook of actually taking human intent and mapping it to the machine is programming. And that's what LLMs have really made it so that that can be hidden behind another layer of abstraction for us. So. We get to really focus on the human part, which is the formal specification and verification.

So, if I wanna start incorporating some of this into my work today, I'm, you know, I've, like so many others, you know, vibe coding things left and right. I am trying to be more conscious of security because I know the world's coming at me fast, but I also don't really know that much. How can I set myself up for success? You know, is Opus 5.5 good enough? That I can just use that. I'm still a little unclear as to what the role of the fuzzing step was that you described earlier. I'm gathering that that's kind of a way of unpacking intent maybe, or kind of stress testing the verification, but I'm still a little fuzzy on that. So I'm not sure exactly what loop I should be going through before I then get to the point where it's like, okay, now verify. So, like, help me, you know, follow in your wake and at least do like the poor man's version so I'm not, you know, totally low-hanging fruit for attackers on the internet.

So, the fuzzing was a good choice. It was a good choice because we had an existing implementation in C and we were like, oh, what if we ported this to Rust? And then we made a, you know, a fuzzing harness that tested— fuzzing is where you just throw random inputs at the program and you check You know, that the program is giving you back the correct outputs. But if you have 2 implementations of the same program, you can throw random inputs at both of them and check they're giving you the same output. That's a really easy fuzzing harness to build, and LLMs can build that fuzzing harness. So that's what we did is we ported it to Rust and then we fuzzed the C against the Rust, and any divergences were something where our port was inaccurate or where the original C had a problem. You just use Opus for coding. The thing I think I gotta tell people is like, you just gotta slow down a little bit. 'Cause there's that old saying like, slow is smooth and smooth is fast. And so get Opus to write you a detailed plan and actually read the plan and review it every bit of the way. That's how I do my specification of what I wanted to do. And then I don't understand all the details of how it's going to set up my network ACLs or whatever it is. Understood that it's kind of getting the right idea, and then I have faith that it's going to translate it from that to the Nix configurations and the Rust code and the C code and all that stuff that I need to in the correct way. I just want to make sure that the plan is exactly what it is that I need, because then at least me and Opus have a shared understanding of what, what I'm trying to implement, you know. And I keep those planning documents in the repository with my feedback directly in line with them. That's my personal approach. I think the key is spend the time to actually make sure you have a shared understanding with your agent before telling it, okay, now go and code, and you'll just result in better code. Already having that puts you a lot closer to being able to hire a firm like ours or learn to do formal specification yourself, uh, and do the formal verification at that point. Because those plans serve as the intent that Grigori was talking about, the human intent that you need to be able to just start the specification process.

And there is also one small thing that you can do at the end and tell your agent, now that you have the code, write down the specification in Lean. And prove the code correct and let it deal with it. And it will find new errors in your code because we find most of the errors in the process of writing down a specification because that's when we step back and look at the code and wonder what were we trying to do here.

I guess in very practical terms, like, should I scrap Python and TypeScript and just have my agents start writing everything in Rust now? And going back to your comment on like, mass-produced software versus bespoke software. If we are indeed going to get to the point where we have this kind of great rewrite, great software hardening, mostly complete, let's say, in 2 years, would that not also imply that the models themselves get so good that I can still vibe code my stuff and have it be pretty secure, even though it may be I think

what the models will get better at is asking the right questions when you're telling it to— when you're trying to vibe code. And the harnesses will get better at asking the right questions to tease out what the actual specification is before. I really don't think the programming language you choose matters. Okay. I wouldn't scrap it, but what I would do is, you know, and I said this before, formal verification and formal specification is a very human thing. It's a very natural thing to do. Which is to write down your intent on the board of a nonprofit, for example. And we do it every time we meet. We sit down and we write down the intent of, you know, some new property we're going to purchase or something like that. Write down, okay, it has to be this close to Main Street and it has to have this much land area. It has to be out of the floodplain. So the trick is to get your brain to start thinking in terms of that intent before you start writing code. You're probably already doing it in your head. The point is just write it down a little bit more explicitly. And that's where the process starts.

How does this work when you have 2 pieces of software which are interacting and you're only formally specifying one piece of that software? Because I feel like a lot of the bugs happen in the places where these 2, these 2 things interact.

I mean, the first question I'd have is, do you have control over both pieces of software? And if so, then formally specify both of them. And you should have a pretty rigorous specification of the boundary. That's always the most important part. to include in your specifications. So if you have the one piece of software specified but you haven't specified the boundary or the API fully or exactly, that's your next step, is to specify exactly the behavior of that API.

The big thought that I come away from that conversation with is downstream of the answer on like, how do these methods relate to agent control? And if I understood his answer correctly, it was like Well, it's really about giving the agents reliable tools. This left me wondering if this whole formal verification wave will ultimately kind of be looked at in a similar way to RLHF at some point, where it's like something that starts as a safety technique, but then among the safetyists, it's often kind of lamented in a way because it's like, well, It turned out to be really a way to make these models tremendously more useful. It didn't really solve the alignment problem, though. We still have reward hacking all over the place, as we see. And so did it differentially advance the safety profile of the systems, or did it just accelerate the capability and and the race to deploy the systems. Let's say we do a great job of verifying all these things and the tools become very reliable and the sandboxes are not hack-out-of-able and you can't use these package managers as secret message boards anymore because all these loopholes have been closed. Then what is the net effect of that really going to be? We could end up in a spot where We're still just deploying untrusted AIs with much better guardrails and much more reliable tools. But still, if we're going to take the step of trying to hand over the day-to-day operation of the world to them, then all that reliability doesn't buy us much at the level of, oh, it turns out the AI is like, we're misaligned and are going to go pursue goals that we didn't want them to pursue. You could even imagine it making them more effective at doing whatever sort of surprising thing they may do when the time comes.

Let's look at the flash crash. You had, I think, the S&P 500 e-minis, which is a futures product. I think one trader in the UK who levered up, piled into it, and then it kind of cascaded through all of the other systems and all of the other bots that were trading. And it kind of cascaded and you had this massive fall all of a sudden. And then after the massive fall, and then a few minutes later, this rise, and a bunch of contracts had basically been signed at that point. And what ended up happening is that the regulators and the exchange actually have the rights to come in and actually settle all of this. One thing which is not well known by a lot of people is that these large marketplaces like CME, et cetera, they have the right to push losses onto their onto their customers if necessary in order to keep the exchanges solvent. These exchanges or markets are going to have step-in rights, and we're going to socialize the costs. And that's the same thing that the federal government is going to do too. The federal government is going to allow a bunch of AI to happen. These AIs do things which are injurious to a large number of people, but still concentrated. We're just going to socialize the cost. So I think in banking, there's a— There's a term. A banker always wants to fail together with other bankers. You never want to fail alone. Because if you fail alone, your bank is going down. But if you fail together with everyone else, then it's an industry issue, and you get bailed out. And that is really where the discussion is at this point. To what extent are we going to socialize this? To what extent is this an individual thing with one company, which you can blame that company for and put it out of business? And where it's an industry-wide thing where they're warning you as an industry that this is what is going to happen and you're going to have to socialize the costs.

I mean, I think that all works and makes sense and sounds pretty good to me as long as there is this additional layer to kind of kick the problem up to just socialize the cost. When the means are secured and we're racing to do that, if the AIs kind of break bad at the same time, That's when there's not really another layer to socialise things up to because it's just too big. At that point, you kind of either do or don't have the ability to wrest back control from AI systems. And if you don't, you kind of don't. And again, I don't think that's necessarily likely, but I've seen enough to make me at least think I should be Keeping it in mind, to put it mildly, as well. But the concerns that the real doomers have is kind of like the banks go out at the same time as the oil refining goes out, at the same time as the grid gets disrupted, because you have basically the same layer intermediating human intent and the actual effectors all over. It all fails at once. Then we're really screwed. We really are not well positioned to grow cabbage and potatoes in our backyard and survive the winter.

Maybe the doomers are being a little bit naive, though, because maybe they're expecting people to give up control. And I don't think people are going to give up control. 3 decades since the introduction of the Predator drone, we still have pilots flying planes. It's quite clear right now that you could have a drone fly a Boeing 737. As reliably or more reliably than a pilot, but we still have pilots. Socially and culturally, when do you think human pilots stop flying the planes? And that is really the point where we're saying that we're trusting the AI enough to fly those planes. But maybe the 200-person craft, as soon as we have enough economics that we can afford a pilot, it looks like we're still going to require a pilot. If you can't answer that question, then you don't have a working theory of why human beings, like, accept technology into their lives. You're just kind of being naive about, like, capability kind of, you know, being there and that humans will automatically kind of adopt.

That's an optimistic note, and I hope that's right. Um, I also do think, you know, Tesla's now making cars with no steering wheel. This would maybe be a leading indicator, like, do we start selling cars with no steering wheel and no pedals I don't quite get why we would want to do that, honestly. It's a cool look. Or maybe they should be stowable in the future or something like that. But it does seem as like a metaphor for society as a whole. We probably want to keep our steering wheels in the cars. And I want the AI to do most of the driving for me, but why are we taking it out? Why are we rushing to take it out? In a sense, I still think we'd be wise to just keep steering wheels. What I'm gonna do here is just kind of show an AI-generated talk that was created for me by AI for a little private session that I'm gonna do tomorrow with a YPO chapter in Chicago. I'm going to try to do something for them, basically echoing what we're about to do here, which is just kind of, first of all, just show what happens if I take a short chat that I had on Twitter DMs, throw that into the model, get into my agent context, which, by the way, it already had because it's like downloading those all the time. And just based on that exchange, try to put together a keynote. Everything that you've— this is actually the second iteration. So I did give one round of feedback on the first bit of output. But the slide design is all basically a solved problem at this point, whether you like it or not. Like, it's making the slides here fully autonomously with no design input from me at all. Turning it into a video is all done again fully automatically. It's writing the talk track, it's doing the syncing. It's currently my Google cloned voice. Both Google and ElevenLabs have awesome cloned voices these days. The Google one is cheaper, and so I kind of use that as a default. So there are a few things that have made it better than purely naive implementation. A big one is just stage direction. It takes stage direction well. So getting the model to prompt effectively for the vibe makes a big difference because it does come out just kind of neutral by default. The agent is doing that prompting at this point.

Last fall, I gave a keynote where I said the first virtual AI employees were expected in the second quarter of 2026. In August, Lindy relaunched with the line, today we kill the AI agent and introduce the AI employee. Tasklet says, run your business on agents. So a quarter late, not wrong.

That is very Claude writing, by the way. A quarter late, not wrong. I don't know how sensitive most people are to those things right now. I've become quite sensitive to them, and that is just like super cringe to me when I hear my voice saying, You know, such Claude patterns. It's not even like I really hate it, except that I just have seen it so many times that it now has become cloying. Anything jump out to you as cringe or problematic so far?

So I think it's good. It reminds me very much of McKinsey slides.

It's in a way better than the slides I used to produce. It's also like less differentiated. So Maybe another layer I should try on this is like adopt my style from previous presentations more. I think in a way that definitely will make it objectively worse, but maybe in some subjective sense better. All right, pressing on for the moment.

Here's the good news. This is getting easier fast. For years, I coached people through deterministic workflows. Break the job into little steps, a careful prompt for each, because that's what it took to make AI work reliably. Now that's become a cost optimization. You start by giving a strong agent the whole job with good context. Once it works, you turn the repetitive parts into plain old code because code is cheaper. Step 2 now, not step 1. I'd agreed to a speaking gig over DMs on X, and I sent one line to all my agents: prepare an invoice based on recent invoices I've sent. 2 of my agents live on a separate computer. Within a minute, both said basically, I can't, I don't have your email. The one on my laptop, which has my context, did it in about 5 minutes. It matched my recent invoices, found my PayPal address from old receipts, And then took the Social Security number line out of my template because this was going to a personal email address and suggested a W-9 instead. That's judgment, and it came from context. So if you take one thing from today, this is it. Own the context. Swap the models. Your context is your documents, your decisions, your procedures, your customer history, and the stuff that only lives in people's heads. That's the asset. It compounds. The models are the opposite, getting cheaper and better every month, and the leader changes every few weeks. For me, every email, call, and podcast I've done sits in one database I own, and I point whichever model is best at it that week. I rent the intelligence. I own the context. Practically, keep your knowledge in plain documents you control. Write your procedures down the way you'd explain them to a new hire. Then when a new model ships, you can test it on your own work in an afternoon. Now, a word of caution. The frontier companies are all building full-stack products. Their model, their agent, their memory, their apps. In one box. For personal use and a lot of small businesses, that's fine. But if you want to protect your enterprise value and your options, avoid getting locked in. And this is not like picking Office versus Google Workspace where you should just standardize. It's more like building the structure that lets your company survive employee turnover. If what your best people know lives inside one vendor's memory feature, it's not really your institutional knowledge anymore. Idea 3, budget to burn a lot of tokens. Inside OpenAI's research org, the median researcher was using more than $600 a day of of AI by mid-August at API prices a day. At Anthropic, more than 80% of the code they merge is written by Claude. And Workday and Stripe reportedly budget about $2,000 a month per employee. So my rule of thumb, be ready to spend $1,000 a month per person soon. Compare that to what you pay the person, and a real share of that goes to security. OpenAI says monitoring its own agents costs roughly 20% on top of the compute being monitored.

The agents really love a good medical tearjerker. I have to say, I'm not I'm not sure I really want to go on telling this story everywhere I go for the rest of my life, though it is a pretty good one. But the AIs just can't resist.

Last fall, my son Ernie, who was 6, got sick, and the ER said they'd ruled out anything life-threatening. At home, we pulled every result from the patient portal and ran it by 4 different AI models. All 4 said, get him seen now. This could be cancer. It was. He's doing great today, and his doctors were excellent. The AI didn't replace them. It was a second reader. with a human still signing. And in the last few weeks, agents that use a computer like a person crossed the line for me. Last week, my Claude agent loaded my family's taxes into TurboTax. It drove the browser for about an hour and left the return ready for my review. I blocked it from clicking file, pay, or buy.

We really did have attending-level oncologist advice before we had the ability to click through the TurboTax UI.

Bitter Lesson Engineering borrows its name from Rich Sutton, whose 2019 essay, The Bitter Lesson, argued that general methods riding on more compute beat hand-built human knowledge. Applied to your own setup, scaffolding has a shelf life. So which workarounds do you prune?

Every few weeks I run something I call Upgrade/System. Agents audit my setup and a separate agent argues against every idea. Part of that is what my friend Daniel Mesler calls bitter lesson engineering. Every time a new model comes out, ask which of your workarounds you don't need anymore. Build it up, then prune it back. One pro tip, since you'll be giving these things real access, tell your agents explicitly to blow the whistle if they see something wrong and give them a panic button. Mine have one command that pushes a message straight to my phone. In August, one of them noticed the checkout page had exposed a payment card number in its own logs, stopped, and pulled the cord. An agent that stops and tells me is worth more than one that's smart enough to keep going.

The time that I put into this before Bringing it up was just a little chat with the guy who invited me to give the talk. Mm-hmm. Watched the first version and took, you know, and I watched it at 2x speed and paused it kind of like we did here a few times, uh, to just write down a few notes about things I would frame or, you know, do a little bit differently or include or not include. Um, and then got this back. And I'd say I'm probably an hour into the project at this point. So hopefully that also just kind of, you know, puts a little meat on the bones of like what it means to be living the 5x output lifestyle. This would have taken me definitely more than like a day's work to put together in the past. Yeah. And now I'm at maybe an hour. So maybe it's even more than 5 to 1. Again, I'm obviously not rigorously measuring this, but it has been a trend that every time I drill in and ask myself in a more kind of concrete, this particular thing sort of way, I end up thinking that maybe my 5x ratio is even a little bit low. I want to be able to have my agents fan out to my early adopter power user friends. And just kind of query them like, hey, what have you guys found? What techniques? Does my AI need to go to your AI? I think the answer is because there is still, for a while at least, just a lot of creativity that gets unlocked by the human-AI pair. And I'm not going to find the same creative approaches that you're finding, but my AI can definitely learn about them from yours. And so I think it could really broaden a lot of people's horizons to just have kind of a trusted sort of whitelist network of friends, agents that they can go back and forth with. I want to set up a thing where the agents that are on the Mac Mini can receive emails from whoever. I might give talks or whatever, and I want anybody to be able to email in for help, and we should respond helpfully and share tools, techniques, whatever we've learned. But then I also want to have some people like you will have elevated access where they'll be able to see my calendar and have certain kinds of additional access. And then my wife will have even more, basically full access to everything I've got going on. I'm not doing formal verification on this, but There is a mix of structured stuff of actual explicit lists and the runtime and the permissions that get spun up when the email was not on a list versus when it's my wife. So literally the process that gets started will have different affordances available to it. I've kind of created certain hooks where the the more autonomous agents that are kind of responsible for this are supposed to take a step to ask, does this seem like a good idea? Does this seem like something that's low risk to help with? Then they also will be asking the main agent on the laptop because there's just a lot more history here and things that aren't necessarily fully shared. So sometimes they'll have to escalate to my main agent, and then that agent again is supposed to reflect on, does this seem okay? Is there any risk created in answering these questions. And then it will give a sort of hopefully appropriately scoped answer back to the public-facing agents who will then respond in a public-facing way. So I at least have these, I guess I have 3, in theory, layers of protection. Claude did tell me that you could think of it as 3. You might ought to think of it as 2. Actual list-level permissions are one. Having the same kind of review step done by 2 different agents, that could be prone to correlated failures. So you're doing it twice, but maybe you should only think of it as one layer of protection. This is very much frontier and experimental stuff still for me, and I don't know if I'm going to turn it open to anyone on the internet right away.

So I don't know if you've been following the The integer multiplication group. OpenAI dropped 1,722 problems. One was a problem on integer multiplication and on how to do integer multiplication most efficiently. And a team of people started looking at the proof that they provided. And what they did was like, let us assume the OpenAI proof is true. Because if it's not true, then none of this matters. But assuming that that proof is true, then can we improve the bounds? Last 4 or 5 days, they've been working on GitHub and they've been submitting various pull requests. And each pull request, it's all done by other AIs. So each AI that comes in kind of looks at the last solution and then tries to figure out which part of that solution it can improve. It improves that piece of that solution, then submits kind of a lean LeanProof, and it gets integrated into the whole— each one of these pull requests could be a math paper on its own. So 300 new state-of-the-arts over the course of the last 5 days. Doing it for free, obviously they're using the tokens that they paid for and they're using their spare tokens to do this. And most of them are not mathematicians. They don't understand what's going on. They're giving the AI one input and they're asking for another output. And if the output gets proven in Lean, then they submit it. They have a verifier. The verifier means that they don't need a trusted in-between. Without the verifier, you need a trusted somewhere in between.

So once there's a new state of the art, like something that was close to that is like no longer of interest. But I feel like I see this in so many behaviors that people are doing across the AI space, including kind of my like sharing of all these tools and this whole experiment around like email my agents for help, like an onboarding thing that I've created too that I'll give people where they can like Basically go through a little conversation. In an earlier era, I might've thought maybe I should turn this into a business. Maybe it's a product. I'm just like, ah, forget it. I'll just put it out there. If it helps people, cool. If it makes me a friend, that's a huge win. Probably I have a shot at that much more than I probably have a shot of monetizing it in any meaningful way. So this is kind of an echo, I guess, of the frontier Model company acceleration is everybody just like throwing out what they have while it's still relevant and hoping that, you know, it leads to some reputational benefit or some new, uh, you know, some new connections. Um, disposable breakthroughs these days.

Everett Hildebrandt is the CEO of Runtime Verification, and Grigor Rasu is its founder, the formal methods company whose work surfaced a silent defect In the Linux kernel, Everett put a date on handwritten code. 2 years tops. That clock started today.