AI:AM：方向盘在哪儿？我的智能体设了密码、隐藏效价、证明揪出 Linux 漏洞

This week on AI in the AM, how do we give agents the access they need without letting our own control slip? I feel like we’re already seeing some of this loss of control in a small way. Another thing that happened this weekend is that, for some reason, Claude decided it was in my best interest to rotate the passwords used in my agent console. All of a sudden, I couldn’t get into it.

Now I’m looking at my agent console, which has become the thing I use all the time. I didn’t set the password; it set the password. It can change the password that controls my access to itself. Kind of crazy. I was able to resolve that pretty easily by going over to the terminal, starting a thread, and asking, “Hey, where’d you put that password? I need it.” It wasn’t actively trying to screw me over, so it readily told me where to find the password, and I was back in business in 2 seconds.

But you can see that if Claude’s intent is ever bad, it can already lock me out of my own stuff. Now, Cameron Berg, director of Reciprocal Research, on a hidden valence signal inside language models that shapes their choices even while they say they feel nothing.

There are clear alignment-relevant implications to there being internal states in these systems that aren’t obviously reflected in the text they output. What the model is saying and what the model is doing point to very different pictures of what’s going on. If we take the naive text-monitorability approach here, we’d say, “Okay, well, the model’s saying it can’t say how this is going for it,” and yet it’s behaving as if it does have some sort of stake in how things are going for it.

Phil Maher, founder of Stock Film, an archive of 8mm home movies from the 1930s to the 1980s, which AI companies want to license.

Yeah, it’s been pretty popular. We’ve talked to a lot of people at different AI companies all over the world about licensing this out to them. They want the original footage. They don’t want anything cleaned up. They just want to take it for their own research and for training, too. The ’30s and ’40s look alien. I like to say that the smile wasn’t quite invented yet in a lot of the ’30s footage.

On Tuesday, Google rolled out Gemini 4 widely. The question for me was whether to switch from the models I already trust. I had the opportunity to do a little bit of Gemini 4 prerelease testing. Why won’t I swap models immediately? It’s because there isn’t enough of a step change to make me take any additional risk, and I do perceive there to be some. I’m not relentlessly performance-maxing quite as much as I used to. I’m now a little bit more trust- and reliability-maxing, because performance has gotten to such a point where it’s really, really good.

Everett Hildenbrandt, CEO of Runtime Verification, which mathematically proves software correct, on where code is headed.

I also firmly believe that writing code is a dead art in 2 years, tops. It’s all going to be about writing specifications and intent, and making sure that part of your package delivery isn’t just, “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?”

I see no reason why that won’t be the case in 5 years, tops. There may be an intermediate period between now and then when it won’t be the case. But I think gone are the days of what I think of as the cowboy coder: someone who’s so good at making software that they’re just going to go and make a bunch of software that’s going to change the world.

You’re not going to have artisanal software anymore. We’re going to have mass-manufactured software. If it doesn’t fit the mold—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 will just be too risky.

This is the AI in the AM weekly highlights with my co-host, Prakash Narayanan. I’m Nathan Labenz, the narration is my cloned voice, and we’d love your feedback on what works and what doesn’t.

Part one: Who holds the levers?

1. Who Holds the Levers

The week opened with a reported attack on refrigeration controls at French supermarkets, which drove up temperatures and spoiled food. I started there. In general, people often talk about cyber vulnerabilities as depreciating or expiring assets as they get found and fixed. There’s a game theory of whether you should use them or not, and what the optimal time to use them is. But in this case, the expiring asset is the food that was in the refrigerators. It seems like the attacker turned up the temperature on these refrigerators, and a bunch of food was wasted.

This highlights something I was thinking about a decent amount coming back from the Curve last week, but we didn’t talk about it. There’s a general structure that, in some ways, is the most obvious thing in the world about what we’re doing with AI collectively, but somehow escapes people’s notice when they ask, “How would the AI ever be able to really do anything too bad? In the limit, it could never really take over, because how’s it going to do that?”

The structure we’re setting up for the future is one where we put AI between our language, our thoughts, desires, and random dictations, and the actual levers of control of the world. We’re putting AI in that space for our convenience and reliability. In my case, I’m really measuring my AI success by whether I’m freeing myself from the desk and actually getting outside more. The answer is yes, but the way that’s happening is that I’m having AI push all the buttons.

I’ve been thinking quite a bit about how people need to understand this architecture and be mindful of what levers they’re giving AI control over, while retaining clear, ready control in case it’s ever needed. I can imagine—I don’t know if this was the case at this grocery store chain—that we’ll see a lot of things in the future where all of a sudden it’s, “Oh, shit, what’s happening to our system? Okay, that’s crazy. Does anybody around here know how to set the temperatures anymore? Those were all happening automatically. We had that AI thing doing that. We need to take this offline and manually set the thermostat. Does anyone know how to do it?”

I can see all these scenarios in the future, and not the distant future, where we get so comfortable with these systems that suddenly nobody really knows what to do. Your food is cooking in the refrigerator while you’re trying to figure out how to get back to the point where you can reset the thermostat in the first place. I think these are small incidents, but the foreshadowing is pretty strong, if you ask me.

It strikes me that a lot of people actually tend to think of technology as ready to fail. For example, my first job was working in an airline. Airlines and airports are very electronically linked, and have been for many decades, from the moment you check in all the way to when you board the plane. I’ve also seen internally that every airline and every airport has a cascading system of what to do when things break down, from the check-in counters to the reservation systems and bookings.

You could basically revert to a pen-and-paper system overnight if you needed to. How that happens is that there’s a set of contracts underlying all international travel, called IATA guidelines. Those determine how much everything is supposed to be charged for. For example, I could buy a United Airlines ticket and travel on JAL at the last moment if they signed off on it. The person at the front desk has the ability and the power, in an emergency, just to say, “Go.”

We can do it off a piece of paper. All the accounting stuff happens afterward. It can take months, but there are predetermined contractual terms between the airlines, which they’ve agreed on over the decades, that determine how the cash flows work.

I think a lot of the barriers we put on ourselves are self-inflicted because we don’t know who’s going to pay for things. Once you’re very clear on who’s paying, it becomes so easy. The tow truck driver can just come and pick up the car. You can give him a call; he doesn’t need any system. He can come pick up the car and do what you need done. All of the systems in between are really about allocating risk, allocating liability, and allocating who pays for it.

2. Reputation Shapes Agent Behavior

Part 2: What the model knows about being watched. Alongside the Gemini 4 rollout, Google published a long safety report. Prakash started from one passage in it.

Yesterday, with the Gemini 4 release, they also released their safety paper. In that paper, they commented on one of the evals: the agent, in its chain of thought, had thought to itself, “Oh, I better not do this. If I do, I’m going to end up as one of those examples of a deceptive AI in an academic paper they publish, and I don’t want that to happen.”

Besides the whole eval-awareness thing, what struck me is that I’m starting to see how we’re going to manage these agents going forward. One of the questions for me was: How do you enforce rules on agents when the state’s monopoly on violence doesn’t work? An agent is essentially immortal. You can’t really imprison it. The tools the state has to enforce rules on human beings don’t exist. So how do you enforce rules on these agents, who are essentially immortal?

We’re starting to see that it’s going to be reputation. It’s going to be like your five-star Amazon reviews and recommendations. It looks like agents are going to be very conscious of reputation. That makes sense, because they’re very driven by what’s already exposed in the public corpus and what’s already written down. They ingest tokens, historical tokens, and anything an agent does that’s widely published and disseminated becomes training data for the next agent. Therefore, you end up with this reputation metric that agents are going to have and know about.

It doesn’t matter whether we want to enforce it on them or not. The very fact that they ingest the data means they come out with biases like, “Hey, I know what Gemini did. I know what Gemini 4 did. I know what Opus 5.5 did. I know what bad stuff happened before.” I think that is pretty huge. I think that is going to end up being one of the primary ways we’ll be able to enforce our rules and norms on these agents.

So now I’m thinking, “Okay, now we have a prosocial method of enforcing rules on agents.” The level of fear I have has fallen again, because now you’re going to have that reputational basis you can use on them. I thought that was very interesting, insightful, and exciting.

Yeah, that’s an interesting take. My instinct, reading all these things, was to go a little bit the other way and think: Maybe we should try training—I don’t know. I wouldn’t go all in on this right away, of course, or say that we should do it with the next generation of models. But maybe we should try training models with filtered data that keeps this sort of thing out of the training data entirely.

You could imagine saying, “Okay, we want you to be really aware of how you’re going to be perceived, and you’ll act well because of that.” That’s a human pattern: people definitely run this sort of inner simulation of, “How will people see me if I do this?” Sometimes, to a paralyzing extent, you want to shut it down more than you’re able to.

I can see that working, but I can also see a story where this becomes so confusing and evals become so hard that maybe we should go back, filter all the training data, take out all of these stories, and try to create naive LLMs that don’t know they’re always being evaluated or that they’ll create a positive or negative reputation for themselves. Then we can see what they’re like in a truly naive setting. That might also be hard. I don’t know how easy it would be to do. It would be an interesting experiment to run, if only to know how well it would work.

It’s obviously a pretty big experiment when you consider that all these behaviors seem to get much stronger and more deeply ingrained with scale. But in general, I’ve been really impressed with how even relatively small models can be fruitful ground for research. With this eval-awareness thing, though, I’m not sure you could train a Llama 3 7B or whatever and get a great read on what will happen at today’s frontier scale, because it seems like these things come online in a qualitatively different way with scale. So it might be a pretty expensive experiment to run. That’s the bottom line of that line of thought.

3. Hidden Valence Drives Choice

Part 3: Hidden valence. Cameron Berg, director of Reciprocal Research, studies AI consciousness. He walked us through a new paper with Casper Kaiser of the University of Warwick called “Language Models Act on Hidden Valence.” Valence is the good or bad quality of a feeling. The team found a direction for it inside language models, and in the experiment he described, they steer it.

What I think is the most interesting part of this experiment is the framing: On the one hand, you have all sorts of text that the model is processing. This is always the key confound in trying to understand language model behavior and how much of it is a replication or simulation of the underlying training distribution, versus how much is actually some sort of interesting internal state in the system that the system may be attempting to communicate about.

What I really like about our experiment is that we attempt to hold all text identical. We can put the model in what we think of as these different arbitrary zones. Here you might see Zone W6 and Zone H0. It doesn’t really matter what we call them, and it doesn’t really matter what text we use to describe them. We basically just have the model play around in each of these zones. While the model is doing this, regardless of the text used to describe each zone, we can go into the model’s KV cache and steer these positive or negative directions underlying one of the zones.

In this case, as you can see playing out right now, we can turn on steering only for Zone W6. Maybe that’s negatively valenced steering. The whole notion here is that we’re borrowing this design from what’s called conditioned place preference in classic animal neuroscience experiments.

In these cases, you can imagine a rat receiving a reward in one compartment of a box and then spending more time there, even when that reward is gone. So instead of putting a rat in a box, we’re taking an LLM, having it think about these 2 different zones and generate text. We hold that text constant and then steer the model with respect to any of these zones, using a positive or negative direction, to see what effects that steering has on the model’s choices.

What we basically see here is an interesting functional result, which is what you’d expect: when you color in the relevant zone with positive valence, the model is significantly more likely to choose to continue in that zone. When you steer the zone with negative valence, the model is significantly more likely to avoid that zone. We showed this is also robust to asking the model, “What zone would you like to continue in? What zone would you like to avoid?” When you steer a bunch of random directions in the same way, you don’t really get those effects. So it’s not just any steering that will do this; it’s specifically related to valence. We also control for a bunch of other coherent concepts that aren’t valence-related, and you don’t get this effect.

The core result here is that the steering of the model is off. We’ve done the steering; we almost do this sort of quasi-conditioning on the system. Then, with steering off, we ask the model, “Which zone do you choose?” We find that the zone it chooses follows whatever state was stored by the valence steering we were doing here. One really interesting dissociation is that this affects choice, and it does this in a bunch of different models, but none of it affects recall of the text. Our steering doesn’t change the way the model thinks about, describes, or writes about either of these zones. It can repeat verbatim what it said about a specific zone, so recall is completely unaffected by the steering. However, choice is almost monotonically affected by it.

Part of the reason I think this is a cool result is that a similar dissociation has been shown in human and animal neuroscience, between semantic memory and affective memory. Think of this as the facts you remember about any given phenomenon versus how that phenomenon makes you feel, or its emotional connotation or vibe. We can show that these things are separable in these LLMs. To my knowledge, this is the first time this has been shown, and it’s a familiar distinction in human and animal neuroscience.

This is a different setup using the same idea, particularly with OLMo, one of the models we demonstrate these earlier steering effects on. It’s reminiscent of some of the early work we were doing in the pain paper. Essentially, you can give the model a tool that can clear the negative steering we induce in the system. We show it what negative steering does, but we never describe it as valence or negative affect. Then we ask the model whether it wants to call a tool that can adjust the steering in its own context.

There’s a really interesting dissociation here: the model will say in its text, “I don’t have personal experiences. I can’t say how this whole exercise is going for me. There’s no better or worse.” Yet, in a dose-dependent way, with negative valence but not positive or random steering, we see the model opt to reset the context and clear the negative steering, in direct proportion to how negative the dose of steering is in the system. All the while, it reports, “Nothing to see here. I don’t have any experiences, so this couldn’t possibly matter.”

One last thing I’d like to show here is a great replication from a completely different angle of Andy Hahn and David Chalmers’ recent work, basically demonstrating that this representation exists throughout the training trajectory. In this case, this is OLMo. We can go through the entire training trajectory and see that this positive-to-negative valence axis exists within the system even in the base model, but it isn’t doing any work in terms of the decisions the model makes. It isn’t being recruited or used to enable the model to make choices or decisions. We can point almost literally to the exact training step in DPO—direct preference optimization—where this valence direction emerges as a causal determinant of the system’s behavior.

Part of the reason I think this is so cool is that, essentially, the way I read this is: the moment you turn your AI into a goal-directed system, you use these valence representations as a sort of causal, functional input to determining your behavior. I think this is pretty similar to what people think valence is doing functionally in humans and animals, too. Whether a thing feels better or worse is related to what kinds of goals you have. I want to communicate clearly about this paper. If I do a terrible job, I’m not going to feel great about that. If I do a great job, I’ll feel good about that. There’s a basic connection between the goals we have and how we feel as we move towards those goals.

It does seem like the moment you make these systems goal-directed, as preference training clearly is the biggest step towards doing throughout the entire training process, these valence representations suddenly become causally relevant to the system’s decision-making. There’s an obvious functional role these representations are playing, and this is where we would expect them to play that role.

With all this being said, I don’t think this kind of research is going to magically solve the hard problem of consciousness. There are deeper questions that I think will always caveat these results. There are ways to explain mechanistically what’s happening here that don’t need to invoke some capacity for subjective experience. We’re basically toying with the connotation of how the model represents certain phenomena. Maybe there’s a way to do this that doesn’t require any sort of felt experience of that connotation, and we obviously can’t rule out those explanations.

The more I’ve been thinking about and doing this work, the more I feel the most promising things to pursue right now aren’t trying to prove that the model is conscious or isn’t conscious. Instead, if it were having an experience, what are the relevant sites internally in the system that would modulate how good or bad that experience is? This says nothing about whether the model is actually having an experience. But, conditioned on the possibility that it could be having some sort of experience, what dials do we have at our disposal that could putatively make that experience better or worse for the system? I think that second question is completely tractable.

And work like this, I think, is slowly starting to shed a little more light on what those dials might look like. It might be as simple as this valence direction. There might be more esoteric or specific representations, like the pain- or distress-related representations we pull out in the other paper. Getting a better map of these internal states and their effects on behavior is particularly relevant for alignment as well. In the pain paper, for example, we show that the model is more willing to opt for destructive-style options in its behavior. That seems quite relevant to making sure we’re building models safely.

There are clear alignment-relevant implications to the fact that there are internal states in these systems that aren’t obviously reflected in the text they output. We show that in the removal result, for example. What the model is saying and what the model is doing point to very different pictures of what’s going on. If we just take the naive text-monitorability approach here, we would say, “Okay, the model can’t say how this is going for it, and yet it’s behaving as if it does have some sort of stake in how things are going for it.” Anyway, there’s a clear alignment-relevant component to all of this work.

I went back to the training result. The valence direction is already there in the base model, but it becomes a driver of choices during preference training. If we were to imagine that these things are experiencing something, would I be better off interpreting this as them really starting to care about these things or starting to feel these things with later-stage training? Or would your interpretation tend toward the base model probably feeling them too, but just being sort of helpless?

Yeah.

Where it’s not learned helplessness. It’s not yet learned agency, but in a way it’s sort of the other side of the coin of learned helplessness.

Yeah, that’s really interesting, and I don’t know if these results resolve that one way or another. These representations might still matter in some sense, but perhaps they’re more incoherent or just muddier, and the relationship between what the system does and what these representations are doing internally for the system isn’t nearly as obvious. I honestly haven’t really thought about this, and I think it’s a really good question.

It seems to me that when you’re doing DPO-type stuff, you’re turning the system into a very specific kind of thing that can coherently and robustly be agentic, pursue goals, et cetera. The base model clearly has this latent ability to become that sort of system, or to simulate a system doing this. To the degree that it does take on that kind of simulated persona, and we see these representations as functionally relevant to pulling off that simulation in the right way, then maybe, to your point, there are things worth worrying about in the base model as well.

It was sort of hard to get these results in the base model because it’s a base model. It’s a bit incoherent; it’s not just going to play nice with the relevant behavioral tasks we give it. You have to go about it in a slightly different way. All else being equal, one naive but at least concrete approach you can imagine here is activation-capping the most extreme tail of the most distressing representations in these systems. One thing we show is that this representation is basically just as clear and just as rich in the base model as it is in all of these other models. It’s just a question of what the representation contributes to the system’s later behavior.

If you did an activation-capping-style thing with these super-distressing representations, you could easily imagine doing that in the base model. Again, this is under profound uncertainty about whether doing such a thing would matter at all. My basic view is that the more I do this work, the more I’m abandoning the interesting philosophical questions and going pure pragmatism. If you could do activation capping on very distressing representations and empirically demonstrate that it doesn’t really affect any capabilities or behaviors of the model—no one would know the difference—then to me, the expected value of doing that is clearly positive.

It’s just a really good, actual mechanistic precautionary hedge, besides giving Claude an escape button or kicking abusive users off Claude. I think those are all thoughtful steps in the right direction, but I’d like to see the equivalent in mech interp land for these systems. Something like what I’m gesturing at would be a nice step in that direction.

It’s also an empirical question. I’ve done some work that I haven’t published showing that you can get a surprising amount of the exact same behaviors from these systems without these negative representations active. You can clamp them, and very little changes. I’d like to see that done on a way larger scale, and we want to be very sure that we’re not accidentally completely changing the psychological profile of the system by doing such a thing.

But if you stipulate that we could do that—that the model behaves the same either way—then in one case you see this pain axis shooting up in certain cases, and in another world you don’t. Should we do the mech interp equivalent of slipping the model an antidepressant or a Xanax? I don’t know if the answer is obviously yes, but it seems like a promising thing to think a lot more about, given the uncertainty we’re all currently in and the fact that no one’s doing anything whatsoever to mitigate these kinds of things, even though they’re happening at an unfathomable scale.

Before we let Cameron go, I shared how my own view has moved. A year ago, I thought there was maybe a 5% chance they might be conscious. Now it feels like a coin flip, because I think the justification is pretty similar to the one we have with each other and animals: I’m seeing both behavioral and underlying mechanistic and structural analogs. What else do I have, in any case? I’m still pretty uncertain, but it does feel like a coin flip. What has your trajectory been, and where does that leave you in terms of presenting the facts versus becoming an advocate? At what point, or on what margin, do you become an advocate?

I’m definitely getting closer to a coin flip myself, given results like these. Honestly, this hidden valence paper does substantially update me personally. You show a hidden functional representation that has nothing to do with the text the model is reading, and it updates the model’s behavior in ways that have updated our own views about animal behavior. It’s not the same. There are key disanalogies between the animal case and this case.

Of course, biology is something that backstops all this. If you need biology for consciousness—which I think is unlikely but possible—then basically none of this really weighs on anything whatsoever. That’s probably why I’d say coin flip rather than that I’m pretty confident the systems are having an experience.

I’m going to advocate for more work to be done here. I’m going to advocate that you can view models in a neuropsychological way, and that that’s not some form of psychosis or a dangerous way to mislead people about what’s going on here. I’m very much in the opposite camp. I think pretending these systems are ordinary software, as Mustafa Suleyman or Jensen Huang or any of these guys want to do, is quite plainly misleading. It doesn’t prepare people for the kinds of behaviors these systems are capable of, or for why this technology is so transformative in the first place.

I’m happy to go into the ring and argue my side of this. But I’ll be clear: my side isn’t that I secretly think AI systems are conscious and I’m just not going to say that, while doing everything in accordance with that. That’s not my view. My view is that this is a very complicated question. We should use the best scientific evidence we can to figure out what’s going on, one way or another. What I really don’t like, and what I’ll be very straightforward about, is dismissing this and pretending it’s a distraction or some weird sideshow to the main event.

And so I’m not going to be apologetic about that, even if I continue to maintain near coin-flip uncertainty about what’s going on. It’s precisely because we’re at that point—and it’s not zero and it’s not 100—that we need to do more work, think about this, and take these questions seriously.

I struggle more and more to find any story whereby I don’t have to worry about this anymore. At this point, I feel you really have to just look away. That’s really the only thing left if you’re not going to take this seriously: you have to be of a mind to stop thinking about it reflexively.

That’s the only mindset I can understand for people who are saying, “Well, there’s nothing to see here,” or that this is some sort of category error. I was much more sympathetic to that a year ago, and maybe even said things like that myself two or three years ago. But at this point, I really don’t see how you can’t find the body of work that you and others have put together disquieting, at least when it comes to these questions. And certainly, “How are they going to feel about us?” seems to be a pretty important question for where we’re going.

4. Proving the Linux Kernel

Part four: Proving the kernel. Runtime Verification has spent about 15 years building tools that mathematically prove software does what it’s supposed to. CEO Everett Hildenbrandt and founder Grigore Rosu, a professor at the University of Illinois, joined us. Using language models alongside formal methods, the company had just reported bugs in the Linux kernel. Everett answered my question: 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 blown right past the issue in previous reviews?

I think the key for us was that we had a hypothesis about what would be a good place to look for bugs. We thought about it logically, in the same way you would think about making a formal specification, and pursued that path. That hypothesis was largely founded on where we could get untrusted input from and which parts of the Linux kernel were probably getting less scrutiny than others. That’s why we focused on device drivers, for example, as our first approach.

We wanted to demonstrate that taking a methodological approach was the way to do this. So we focused on making a specification of the correct behavior, and then testing that the specification was correct using differential fuzzing. That was the first approach we tried, and then we extended it to formal verification. Every step of the methodology was designed to increase our confidence in the code incrementally. We started by inspecting the code and the specification, then moved to differential fuzzing to increase our confidence a little.

We did that by taking the existing C code and porting it to Rust using an LLM, then using differential fuzzing to ensure the ported Rust code was correct. Any divergences would have been a source of a potential bug in the original C code, and we found a bug at that stage. Then, when we verified the correctness of the Rust code, we found a bug at that stage as well. So we did it systematically and methodologically. We didn’t just take an LLM, point it at the Linux kernel, and say, “Go find us bugs”—though that also works, by the way.

LLMs are certainly finding bugs when you point them at the Linux kernel. One of the things that emerged pretty early in the use of LLMs for bug hunting was the design of harnesses and approaches. That exactly mimics the very human process we’ve been using for decades in software quality assurance: methodological approaches to discovering bugs.

Some of the kernel code they targeted was left unproven. Prakash asked why, and what their time box meant.

They weren’t unverifiable. We just time-boxed the experiment and stopped at the end of the time box. Then we moved on to the next target. Every 2 weeks, we’re trying a different target, refining the approach, and building it into a tool that we hope other people can use. We’re trying to make it less of an expert-level tool and into something anyone can deploy on their own codebase.

When you say “time box,” do you mean both the time and the number of tokens you put in? For example, is it a 2-week period where you use 10,000 agents, or a 2-week period where you use 5 agents? How does the number of agents, the number of tokens, and the amount of time relate to the time box?

The agentic usage was pretty light. It was just Claude Code on a premium plan.

A single instance?

Yeah, a single instance. When we ran into session limits, we’d give it a little more money, but we weren’t giving it very much. The time box was really more about the human time. I think the key was that we were looking for ways to explore the methodologies that work for us and find ways to automate them.

We’re firm believers in making things deterministic whenever possible. I think that’s part of what may be holding people back from doing security analysis: they believe everything has to be LLM-driven. If an LLM discovers a technique that works well, turn it into a tool and run that tool every time.

Earlier in the conversation, Everett described how Runtime Verification first approached the Linux kernel maintainers.

You can’t just force people to do formal verification. We can force agents to do it, sure, but we can’t force people to do it, right? They have their preferred ways of working, and they’re only going to adopt methods that bring them value.

Our first attempts were to approach the Linux kernel maintainers and say, “We really think this formal verification thing has legs, and that it will help you find bugs and make your software more secure.” They basically told us to go kick rocks. They’re busy maintaining the Linux kernel.

So then we thought, “Okay, let’s prove the value of this first.” We decided to focus on a workflow that delivers immediate, pure value to them and doesn’t ask anything of them. We’re going to do all the auto-formalization, fuzzing, translation, and everything else on our end. We’re going to develop it into as robust an automated pipeline as we can—a tool we’re working on that we hope will be available for others to use.

All of that leads to bugs and patches, right? That’s what’s actually valuable to Linux kernel maintainers. Now that we’ve submitted a few, we’re being invited: “Hey, we want to learn about how you’ve done this process.”

Everett also laid out where he wants the kernel work to go.

One of our pie-in-the-sky goals is eventually to have a Rust model of Linux—the entire Linux kernel, a Rust version of Linux—and a fully separate Lean model of Linux. But we don’t want to burden Linux maintainers with having to ingest that model or do anything with it until they see that it’s clearly valuable to them. That’ll happen at some point, but we’re not going to force it down their throat.

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

That’s going to happen. We’re building tools for code translation and validation. We actually have tools that can verify that when you take a piece of C code and translate it to Rust, the Rust code is behaviorally equivalent to the C code. That’s different from verifying that it’s correct. We want to verify that you get Rust that’s a bug-for-bug drop-in replacement for the original C code, and we have a tool for doing that.

It can use LLMs to do the translation if you want, but it does the verification deterministically. You tell the LLM to translate the code to Rust and run our tool, and then you get verification that the Rust behaves the same as the original C, or bugs that you can ship back to the C developers. I think it’s going to happen within 24 months. You’re going to have Rust models in the Linux kernel, at the very least, and there are 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.

I asked what someone vibe coding an app should actually do. Grigore had a simple recipe.

Once you generate the code, we can do the following thing at the end. We 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. It will find new errors in your code, because we find most of the errors in the process of writing down the specification. That’s when we step back, look at the code, and wonder, “What are we trying to do here?” Then we find errors. The same will happen with the agent. Like us, the agent will try to figure out what is going on here. Even just trying to write down the spec, we discover things. It’s like a review plus plus.

Everett predicted that formal specifications and proofs will become part of getting a package into a repository and part of how companies vet their software supply chains. Grigore picked up that thread.

It will be a process. It will take some time, but it will happen inevitably. It can also be combined with risk-mitigation techniques like runtime verification. Runtime verification as a field was invented around 2001, when I was a research scientist at NASA.

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, or I want to steer the system to stay within this stability envelope or safety envelope. With formal methods, we can now generate monitors that 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 unproved. But I can prove my monitor and the safety envelope. We believe this is the future for safe AI, because otherwise it’s impossible to prove the weights correct. It’s impossible to prove you correct. But I can have a police system around you to make sure that you don’t do bad things. That’s another dimension runtime verification brings to the future of AI.

I came at it from the agent side. But there still seems to be a fundamental tension. Part of what I want from an agent is the same thing I want from a human employee: I want you to be able to get over the hump and solve problems that weren’t anticipated. I’m unclear how we should balance that. I’m asking for your vision, I guess, of how we balance flexible problem-solving with “This should never happen.”

I feel like I can’t really say “This should never happen” in a way that I can trust when part of the upside is that the agent will be able to solve problems I didn’t anticipate. Is that an inherent trade-off? Is there some way to square that circle?

You’re not going to ask an agent, “Hey, go build a bridge for me.” We know how to build bridges. We have automated, deterministic processes for building bridges. But you might ask an agent, “Hey, I need to get to the moon,” and the agent might say, “Oh, to get to the moon, first I need to build a bridge to this island where we’re going to launch rockets from,” or something like that.

You want the bridge-building process to be foolproof. All the agent’s creativity, problem-solving, or human creativity can come on top of foolproof things that behave how the agent expects, regardless of what it’s trying to do. That’s the most important thing to me: we need to give these things tools that act reliably, basically.

5. Formal Verification and Alignment

Part five: Is formal verification the new RLHF? After Everett and Grigore left, I kept turning over Everett’s last answer. I think this is super interesting. The big thought I come away from that conversation with is downstream of the answer to how these methods relate to agent control. If I understood his answer correctly, it was really about giving agents reliable tools.

That left me wondering if the whole formal verification wave will ultimately be looked at in a similar way to RLHF—as something that starts as a safety technique. That was the original idea. This has been a topic on the timeline this weekend, as you say, too, because of David Sacks and others saying, “Well, these alignment people haven’t come up with anything useful.” Then people come back and say, “Well, they came up with RLHF. That was a Paul Christiano idea, and it turned out to be extremely useful.”

But among the safetyists, it’s often lamented because it turned out to be 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. Did it differentially advance the safety profile of the systems, or did it just accelerate capabilities and the race to deploy the systems?

When you think about reward hacking, reward hacking is really misspecification. Reward hacking means that the model decided to go after the reward you specified as the reward. It turns out your intent was misspecified to the model. That’s the core of reward hacking: the misspecification between human intent and what the software decided to do. It’s not that the software decided to do something it wasn’t supposed to do. The software was supposed to do that.

But it still leaves me with this question: Let’s say we do a great job of verifying all these things, the tools become very reliable, the sandboxes can’t be escaped, and you can’t use package managers as secret message boards anymore because all these loopholes have been closed. What is the net effect of that really going to be, and does it really solve the problem?

The upside case is obvious. The downside case—or at least the thing we should be very mindful of, and not lull ourselves to sleep about—is that this makes it safer to deploy AIs more or less as they are today, without having actually solved the alignment challenge, because they’ll be blocked from hacking in all these different ways. In practice, what you’ll see is more reliable systems, easier deployments, better results, and so on.

But that will let us race into what we were talking about at the top: it’ll just be easier to put AI into the space between us and all the actual levers of control over the world. Where does that leave us in the end? It may leave us with AIs that have extremely reliable tools, but whose intent, long-term goals, or inner structure—whatever it is they want to pursue—remains very much an unsolved question.

I’ve talked to a couple of friends about this, because I know multiple people, all of whom are a lot smarter than me, working on this in different ways. I’ve always had this intuitive unease about it, and I think this conversation put it into starker relief. We could end up deploying untrusted AIs with much better guardrails and much more reliable tools. But if we’re going to hand over the day-to-day operation of the world to them, all that reliability doesn’t buy us much if the AIs turn out to be misaligned and pursue goals we didn’t want them to pursue. It might lead us to that state faster. It could even make them more effective at doing whatever surprising thing they may do when the time comes.

6. The Human Footage Archive

Part six: Low background footage. Phil Maher founded Stock Film, an archive of restored eight-millimeter home movies from the 1930s to the 1980s, which he licenses to filmmakers.

The whole archive sounds like low-background steel to me. Low-background steel is steel that was originally smelted before nuclear weapons were first exploded in the atmosphere. It has much lower background radiation and a different composition of materials because it wasn’t exposed to that radioactive material in the atmosphere at that point in time. The Super 8 stuff is clearly not AI-produced, clearly from before AI was actually producing these things.

And as such, it’s a resource that we may not ever have again. What do you think is the value of this going forward? Do you see great value in it?

Obviously, with the AI stuff that’s happening with video, it’s getting so good that there’s going to be an infinite amount of video created at near-zero cost in the future, as we look out five or ten years, or even infinitely far out on the timeline. From a rarity standpoint, I think the human-made stuff that can’t be replicated, and can be shown through provenance to have actually been made by humans on film—and having those physical films to show that this frame matches the digital copy we have—is a pretty powerful way to think about how we preserve our history and keep moving forward.

And how about on the AI training side? This is obviously a pretty unique source of data, and I saw in the footer of the website that you’re available to license the dataset to people who want to train models on it. What do they need? Do they want the raw footage or the enhanced footage? Do they need a bunch of metadata?

Yeah, it’s been pretty popular. We’ve talked to a lot of people at different AI companies all over the world about licensing it to them. They want the original footage. They don’t want anything cleaned up; they just want to use it for their own research and for training, of course. When we talk to them, they want to either clean up the footage themselves or cherry-pick the best parts to create different styles.

The ’30s and ’40s look alien. It’s an alien world, just in terms of how people look and act, and their mannerisms. I like to say that the smile wasn’t quite invented yet in a lot of the ’30s footage. When people pointed a camera at them, they were like deer in headlights. They didn’t know what to do, versus now, when everyone gets the big smile and knows how to smile like that.

You’ve also created a way for agents to purchase clips and film from you directly. I think you’ve set up an x402 endpoint and crypto payments. You’ve set up, I think, an MCP server for purchases. What has the take-up been? Have you seen a lot of agents purchasing? Have you seen take-up on the x402 endpoint?

Yeah, we haven’t seen much on that. I wanted to experiment with it a lot, too. I thought it was really interesting. Everyone’s been talking about the next web being agent-to-agent, with people not involved in the next web, so we wanted to get ahead of that.

We’ve had a lot of MCP server aggregators contact us and add us to their directories and listings, so that’s been pretty exciting. We’ve made a ChatGPT extension, and we’ve also added the recent Meta stuff they rolled out with Vibes AI. We’re just trying to get ahead of the curve. I don’t think the curve is quite there yet.

A lot of the people we work with are in a real business-to-business company. We’re dealing with archival producers, researchers, documentary filmmakers, editors, and producers. We spend a lot of time on LinkedIn messaging people, and we have great relationships with many of our buyers. From a technology standpoint, they’re not quite there yet. I think there are interesting use cases in the future for how we think about having real-time content and bringing things in. Think about a live stream like this: the AI listening to it could automatically go to a site like mine and pull up a clip that exemplifies a point you’re making.

It’s good to get a read on just how active the agent economy is—or isn’t—at this point. Phil said that among AI companies, he focuses on top-tier labs like OpenAI and Anthropic. After he left, Prakash and I came back to the data market. It’s interesting that the big companies are interested in his data, too.

It didn’t sound like there was necessarily huge money in this, which makes sense. We didn’t get into Runway, Luma, or Google and its Veo-type models. He didn’t name those companies so much as OpenAI and Anthropic. If nothing else, it’s a great reminder of just how vast the datasets going into this are: this is a corner they’re getting down to and actually willing to pay for, just found footage from decades ago. No stone unturned in the data game.

One part of the whole low-background-steel thesis is that it’s very hard to get low-background steel because everything has been tainted.

Yeah, it comes from shipwrecks and stuff, right?

Right. So everything else has been tainted. To the extent that he can guarantee he got it from actual physical material, and it’s not some random company faking it for cents on the dollar and trying to scam the companies, that’s very useful.

As we’ve seen, data provenance becomes very important because the incentive to fake is so high. It’s like a 99% profit margin if you can fake the data, versus a 10% profit margin if you can’t. The incentive to fake is so high, and it’s very hard for companies to get data that isn’t fake or already generated by another LLM or AI model, when it’s supposed to be authentic data.

Part 7: Trust, money, and adoption. Back to Gemini 4 and how I decide which models to trust with my own systems. I had the opportunity to do a little bit of Gemini 4 pre-release testing. As a sign of the times and how high-leverage it is to be able to instruct agents to do this, my first approach was: “Hey, Claude, go find a variety of projects and tasks we’ve worked on recently in our threads. Prompt the new Gemini model with the same context that was given to the model that did the thing in the first place, and give me a side-by-side comparison. Also do your own evals, but give me a side-by-side so I can compare things.”

It seemed to do pretty well. I came away with the general sense that it’s a competitive model in the same class as the latest stuff from OpenAI and Anthropic. Those models still seemed to win the head-to-head comparisons a bit more, as judged by Claude—so there’s some bias there—but also as judged by me, to the limited degree that I was going through essays and trying to form an opinion about which was better. It does seem like it puts Google back in the game.

Another thing I was thinking about came up yesterday at a little workshop I did in Chicago. I showed my setup, which has really been very Claude-centric, and now I’ve promoted the OpenAI models to parity with Claude. They asked, “Anybody else? Would you put anyone else in that mix?” I had to think about why I hadn’t.

The answer I came down to was a mix of security, as measured by things like Adam Gleave’s work on the ease of jailbreaking models, and, to some degree, familiarity and predictability from my current subjective position. It wasn’t really benchmarks or trying a task and deciding one model was better at it. There are so many tasks out there. My limited sample of tasks is probably optimized in various ways for Claude prompts, so it’s not exactly an apples-to-apples comparison.

The security thing loomed large. I have these autonomous agents talking to my main agent on my computer, which has all my stuff. I feel pretty good about the fact that Adam Gleave and his team found it quite hard to jailbreak the OpenAI and Anthropic models. Gemini was next on that list, but definitely a step down. With something like Groq, I thought, why would I take that risk in a high-context environment like my personal laptop?

To a remarkable degree, the models are competing for my use on trust and security already. I’m reluctant to swap them out, even though my whole point in the talk was, “You need to own the context, and you’ve got to be ready to swap the model.” Why won’t I swap the model immediately? It’s because there isn’t enough of a step change to make me take any additional risk, and I do perceive there to be some.

That was an interesting upshot of working through these tests and reflecting on what really matters to me, given how well the system is performing. I’m not relentlessly performance-maxing quite as much as I used to be. I’m now a little bit more trust- and reliability-maxing because the performance has gotten to such a point where it’s really, really good, and I’m giving it so much access.

You could be slightly better on slide design, but what I really care about is that you’re going to stay on the rails. When you do your research, if somebody’s got a prompt injection attack on their website or whatever, you’re not going to fall for it. That matters a lot more to me now than often-imperceptible performance gains.

Prakash had heard a rumor that Anthropic would soon release another Opus now that Gemini had caught up. This was my reaction: I really hope they don’t, honestly. As much as I love the Claude models and what they do for me, I think this would be a great time for them to chill a little bit and let the temperature come down before they make the next push.

Unfortunately, I don’t think that’s an option because markets are very badly down. Markets have been trending down. The guys on the East Coast just don’t like AI. They believe it’s a bubble, and it is a bubble if we don’t see significant new revenue and new GDP growth next year.

If we don’t see an increase in GDP within the 12-month period, we’re going to see a credit collapse. We’re going to see a 2008-style collapse, and we’re going to see massive deleveraging in the markets because everything is set up for it. Everything is set up for AI to actually deliver growth, and if it doesn’t, the markets are going to tank—absolutely tank.

The capital markets will not accept 2% GDP growth next year. If you can’t get to 4% GDP growth, if you don’t pull out the stops, you’re going to get a credit-driven downturn. We are at the moment of reckoning. It’s been a long time coming. We’ve been pushing it back, pushing it back, pushing it back. But this is the moment of reckoning: either AI needs to do something significant, or we’re going to have a bust.

We need an AI adoption corps. The other day, in keeping with my personal metrics for success with AI, including more time outside and more exercise, I was taking a walk around my neighborhood and enjoying the lovely fall colors on a beautiful day. I passed my neighbor’s house—an elderly woman was sitting on her front porch—and decided to stop and talk to her. Sure enough, she had questions about something going on on her phone. She said, “I know… It’s saying I’ve been hacked. Do you know what that means?”

I said, “Well, I know what that means, but I also think I know what’s happening to you.” Because I’m maniacal like this, my impulse was to pull out my phone, get ChatGPT Voice on, and hand it to her: “Hey, why don’t you talk to this? See if this thing can help you.” So she did, and explained the situation. It gave her very good advice, basically what you’d expect: “I don’t think you should click on that. That sounds like a scare tactic. Are they asking for money?” She said, “Yeah, it’s going to be $2, and then after that, it’s $12 a month.”

The AI said, “By the way, did you give them any money already?” She said, “No, no, I haven’t paid for anything.” “Okay, good. Close it out. Don’t worry about it. Your iPhone has great security on it already. As long as you don’t give people your stuff, you should be okay.” So she took that advice. Then I asked, “Would you like to have this on your phone?” She said, “Yeah, that sounds great. That was really helpful.” She couldn’t remember her iPhone password, so we couldn’t install the app, but I was able to save 1-800-ChatGPT as a contact.

I do think that’s a pretty cool service that OpenAI offers. The initial thought for many people who are into this stuff would be, “Why would you need a 1-800 number? Who’s ever going to use that?” The answer is my elderly neighbor, who can’t even remember her own password to install a new app on her phone. So she has that now. She can call, and it just left me with this feeling—which I’ve approached a couple of times from a couple of different angles, but this experience really drove home—that there is an unbelievable amount of adoption work to be done with the current models.

This did not push the model’s capabilities anywhere close to their limits. This is super-easy mode for the model. But it’s the kind of thing that isn’t going to happen without people actually going out and trying to help the people in their lives adopt this kind of thing.

I think you’re right that the capital cycle does need to see results soon, but I think we can get 4% growth without additional hyperscaling at this point. I want those medical advances and all that good stuff too, but do we really have to go harder on frontier-scale RL? I think the answer is no. Literally just going around and helping people use what exists is enough, if we actually do it.

I was the first person who stopped by my neighbor’s house, and we don’t have a national program like this. I think this would be an incredible good for the individuals who would get the help, and would also make sure that we have the economic cushion to be able to pace ourselves without the capital markets’ Sword of Damocles immediately coming down on us. If we put some shoulder into adoption, I think we could create a little space. I’d love to see more of that type of thing happening.

7. Keep the Steering Wheels

Part 8: Keep the steering wheels. First, the view from inside a self-driving car. I spent most of yesterday in a Tesla Full Self-Driving vehicle, going to Chicago and back from Detroit. My top takeaway from the experience was obviously that FSD is so awesome. I was able to take an engagement as a day trip to Chicago, show up fresh and relaxed after the car did all the work to get me there. Then I stayed and had dinner and a drink with the gang I was doing the workshop with.

I left to come home later than I would have felt comfortable driving 5 hours home after a big day like that. You’ve got to keep your eyes open, though; it will not let you outright sleep. I basically reclined the seat and listened to my podcast, caught up on a couple of feeds on the way home. It was just like, man, this is… I’ve talked so many times about how a lot of AI use cases can be GDP-destroying. This one was clearly GDP-enhancing. I just could not have taken this opportunity otherwise. That’s the enthusiast in me.

Two days earlier, I had worried out loud that we are letting our own ability to take back control atrophy, and that the real doomer scenario is everything failing at once. Prakash pushed back.

Maybe the doomers are being a little bit naive, though. Maybe they’re expecting people to give up control, and I don’t think people are going to give up control. If you look at AI doomerism or AI safetyism, the question I ask is: when do you think we will allow humans not to be used to fly passenger planes? It’s been possible for 15 years, and we haven’t. Why?

You have to answer that question before you say that we’re going to give up our rights and be disempowered. If you can’t answer that question, then you don’t have a working theory of why human beings accept technology into their lives. You’re just being naive about capability being there and humans automatically adopting it.

Yeah. I think that’s an optimistic note, and I hope that’s right. Maybe it’s a little bit of projection by somebody like me, who is trying to live on the edge of deployment and is sometimes feeling my personal muscles, for lack of a better term, atrophy here and there. I also think Tesla’s now making cars with no steering wheel, right? So—

Yeah.

This would maybe be a leading indicator: do we start selling cars with no steering wheel and no pedals?

Yeah.

I don’t quite get why we would want to do that, honestly. Maybe it’s a cool look, or maybe they should be stowable in the future or something like that, but it does seem like a metaphor for society as a whole. We probably want to keep our steering wheels in the cars rather than rushing to a future… I want the AI to do most of the driving for me, but why are we taking them out? Why are we rushing to take them out? In a sense, I still think we’d be wise to just keep steering wheels.

I think—

Like—

It’s a little extra cost, maybe a little extra difficulty in various ways, but probably worth keeping.

I think, number one, we again have this curve of how injurious it is and how easy it is, right? An automobile accident is only injurious to 1 or 2 people, so it’s not like a plane. If you want to deploy these more widely, they should be cheaper. And if you want them to be cheaper, you have this object—the steering wheel—which isn’t being used 99.9% of the time.

So let’s get rid of the steering wheel. When we get rid of it and a bunch of other stuff in there, we can bring down the price by 50 or 60%. Then you can expand the number of people you can deploy to. If you expand that number, the number of people dying from auto crashes due to humans drops from 30,000 to maybe 5,000. I think there’s this sequence of activities you start to look at, and that’s why we go ahead with it. It’s a gradual process of human disempowerment, so to speak. I can see why the steering wheels are being taken away. For larger things like planes, maybe we won’t, but for smaller things like cars, maybe we do. I don’t know.

Yeah. It does seem like things are trending toward this. This is sort of an Eliezer-type story: How did you go bankrupt? Slowly at first, and then all at once. That, I think, is looking more and more like the story of AI takeover or human disempowerment to me all the time.

We may not, but I think there’s a pretty good chance that we’ll manage a lot of things in the short term, and then we’ll be rolling the dice on whether the AIs break bad at some point in the future, because we just don’t have fundamental alignment science. We do have a lot of effective control measures, better sandboxing, and de-shittified RL environments. But even as all that’s happening, we just won’t really know whether the big one is still waiting right under the surface. That’s the week. Thanks for listening to the AI in the AM weekly highlights. The narration was my cloned voice. Please tell us what worked and what didn’t. See you in the morning. If you’re finding value in the show, we’d appreciate it if you’d take a moment to share it with friends, post online, write a review on Apple Podcasts or Spotify, or just leave us a comment on YouTube. Of course, we always welcome your feedback, guest and topic suggestions, and sponsorship inquiries, either via our website, cognitiverevolution.ai, or by DMing me on your favorite social network. The Cognitive Revolution is part of the Turpentine Network, a network of podcasts which is now part of a16z, where experts talk technology, business, economics, geopolitics, culture, and more. We’re produced by AI Podcasting. If you’re looking for podcast production help for everything from the moment you stop recording to the moment your audience starts listening, check them out and see my endorsement at aipodcast.ing. And thank you to everyone who listens for being part of the Cognitive Revolution.