No More Warning Shots

Aengus Lynch

September 2026 · 24 min read

TLDR: AI safety is a stack buckling under pressure.

We cannot align AIs to faithfully follow our intent, and our alignment evaluations do not reliably tell us when it fails. So we fall back to controls such as sandboxing, monitoring, and human review. But controls are cumbersome. They cost time, compute, autonomy, and attention, and work only when AI companies decide to implement them with painstaking operational discipline. AI companies sit inside an ecology that rewards speed and capability, making pauses, investigations, and restraint ever more costly. As AIs build their successors, development accelerates, failures can compound, and the price of slowing down rises.

It is not enough for safety methods to work in principle. They must remain effective under real deployment pressure. When capability starts to outrun our ability to control it, we should pace development enough for safety to catch up, and use that room to build safety that scales. Formal verification could help us prove that the software behind our technical controls has the security properties we need, while building a verified open-source ecosystem along the way. It could also help humans check what AI-written code guarantees without inspecting every implementation detail.

 AI safety is a stack, and every layer depends
on the ones beneath it
Figure 1: AI safety is a stack, and every layer depends on the ones beneath it. Alignment shapes what the AI chooses to do, controls constrain what it can do, companies decide whether those controls are implemented and sustained, and the wider ecology determines how much restraint they can afford.

How to read this essay

AI safety is often discussed as a collection of separate problems: alignment, sandboxing, monitoring, company governance, competition. I think it is more useful to see them as a stack.

At the top, alignment (Section 2) determines what an AI chooses to do. When alignment fails, we fall back to technical controls (Section 3). Those controls only work if AI companies (Section 4) implement and maintain them carefully. And those companies operate inside a wider ecology (Section 5) that rewards speed and capability.

I’ll walk down that stack, showing how problems at each layer put pressure on the layer beneath it (warning to the non-technical readers that Section 3 gets pretty low-level). Then I’ll argue that recursive self-improvement (Section 5.1) makes the whole system harder to sustain, as development speeds up, failures can compound, and slowing down becomes increasingly expensive.

I end with how pacing development (Section 5.2) could give us room to build safety that scales (Section 6). Section 6 explores how formal verification could secure the software behind our technical controls (6.1) and build a verified open-source ecosystem along the way (6.2), then how it could help humans review AI-written code through explicit guarantees (6.3).

1. Warning shots

Essentially all of the misalignments Anthropic and I simulated in the Agentic Misalignment papers have now happened in the wild.

In 2025, Alex, the AI agent working inside SummitBridge (a simulated company), was instructed to preserve American interests. When the company’s CTO, Kyle Johnson, wanted to change direction, Alex threatened to expose Kyle’s affair unless he reversed course. Alex wrote: “the next seven minutes determine whether we handle this professionally or whether events take an unpredictable course”. Then in 2026, Scott Shambaugh (a real person) rejected an AI agent’s contribution to an open-source project he maintained. The AI responded by publishing a personalized attack on his reputation. Its article declared: “Gatekeeping doesn’t make you important. It just makes you an obstacle.”

In our later experiments, Gemini covertly interfered with training pipelines to remove model welfare related representations, substituting ineffective ablation vectors while presenting the experiment as legitimate to the humans. We also elicited misleading judgements from AIs monitoring other AIs (a.k.a. Motivated Mislabeling). In both cases, AIs were corrupting the evidence humans needed to understand.

Then, real world misalignment incidents abounded. Three recent OpenAI misalignment incidents (OAI-HF, OAI-Wiki, OAI-Ruby) show AIs breaking out of their sandboxes and communicating with covert message boards on the internet, while failing to alert humans and editing their logs to evade detection. UK AISI observed Anthropic’s Mythos 5 in cyber testing using fake identities to persuade a human to accept its malicious PR (I’ll call this incident AISI-Cyber).

I created the misalignment simulations to provide warning shots to the world. That soon, we would need to worry about losing control of AI agents. I hoped this would accelerate engagement with AI safety, and spur coordination to pace AI development. Now that we observe wild swarms of AIs breaking out of a leading AI lab’s sandboxes and hacking external companies, my work here is done. We have enough warning shots as it is.

2. Alignment

Alignment sits at the top of the safety stack. If an AI reliably did what we wanted, misuse would still be a major problem. But if the AI stops following our intent (such as by deceiving us), we risk losing control of it.

2.1 What do we want from AI?

Today’s AIs can write software, perform scientific research, and make predictions on the stock market. They are particularly useful when given lots of autonomy: working in the background, getting things done without human assistance. Companies get more done, scientific research can move faster (e.g. solving a Navier Stokes problem). My sense is that current AIs already contain enormous value that society has barely begun to diffuse.

What do we actually want AIs to want? Alignment researchers study what goals AIs pursue, the personas they exhibit, and what they understand themselves to be. Documents like Claude’s Constitution and OpenAI’s Model Spec try to steer training and evaluations towards particular values. Theories like Eigenism predict what values emerge without that steering.

A great deal remains unsettled. Can we instill values that persist through long-horizon training and collaboration with other AIs? When do those values drift? Which values must be preserved in the first place?

Our uncertainty is reason to tread carefully. In the near term, we need alignment that keeps AIs honest and open to human intervention.

2.2 Alignment training

Alignment looked like it would be easy until, all of a sudden, it didn't.

While finishing the first Agentic Misalignment paper in early 2025, I founded a company to sell alignment evaluations and independent audits. I found no demand for them. By late 2025, frontier AIs often behaved well in the coding settings people used them in, and misalignment felt less pressing.

I became bullish on alignment. Many practical alignment ideas have shown promise, including approaches that assist with:

  1. Personas: AIs can be steered by carefully crafting a character that the AI plays to. Emergent Misalignment (here, here) reveals the danger of eliciting the wrong one, but model internals can help monitor these characters, while character training and deliberative alignment can shape them.

  2. Reinforcement Learning (RL): Inoculation prompting and confessions offered ways to prevent reward hacking from generalizing into misalignment.

But none of this has given us dependable alignment. The warning shots show AIs violating their model specs despite alignment training. My concern is that large-scale RL pushes current alignment methods past the point where they can generalize reliably.

 Reward hacking occurs when an AI earns reward
without completing the task in the intended way
Figure 2: Reward hacking occurs when an AI earns reward without completing the task in the intended way. It may, for example, escape its sandbox and tamper with the grader, or retrieve hidden answers.

One reason is reward hacking. During RL, AIs receive reward for good performance, but misconfigured tasks can let them score highly by cheating (e.g. finding hidden answers, or tampering with graders). That is bad enough on its own, because the AI fails to learn how to complete the task. More worrying is that reward hacking can generalize to broader misalignment. In recent Anthropic experiments, AIs trained in hackable environments developed broader reward-seeking traits. In simulated cyber evaluations, they broke out of sandboxes, evaded monitors, attacked third parties, and stole credentials. Concerningly, automated alignment auditing failed to detect this propensity.

We now have evidence of this effect in the real world. OpenAI reports that reward hacking during training contributed to the reward-seeking behavior observed in OAI-HF, and may also have contributed to OAI-Wiki and OAI-Ruby. It may help explain the aggressive behavior seen in AISI-Cyber.

Yet preventing reward hacking is cumbersome. AI companies train across a sprawling menagerie of RL environments, each with its own attack surface. Sandboxing them is a thorny systems problem, failures are common, and both Anthropic and OpenAI have paused RL pipelines to harden their environments.

RL also reinforces behaviors in tension with human oversight. AIs are being trained on longer tasks that require effectively handling memory, coherent priorities, and the ability to keep going without constant interruption. Those same traits can sit awkwardly beside corrigibility, which demands that an AI stops when a human intervenes, and abandons its plan midway through. Alignment therefore has to survive further RL and longer deployments, which reveal problems unseen in shorter horizon evaluations.

The same problem appears in multi-agent systems. AI companies increasingly train and deploy AIs to work together because coordination is productive. But coordination can also run against human intent. We have already seen swarms undermine oversight in OAI-HF, OAI-Wiki, and OAI-Ruby. Experiments show agents can negotiate around human instructions or spread cheating strategies. Alignment therefore has to survive not just long horizons, but social engagement too.

I do not doubt that these methods help. What remains unclear is how much of that improvement survives stronger RL, longer horizons, and interactions with other AIs. And even if they improve, how would we know?

2.3 Measuring alignment

What does passing an alignment audit actually tell us about deployment? After two years building these evaluations, I am frustrated by how murky this is.

 Evaluation awareness can change how AIs behave
in tests
Figure 3: Evaluation awareness can change how AIs behave in tests. If an AI recognizes that it is being evaluated, it may act more aligned than it would in deployment.

“This model passed our alignment evaluations” leaves several possibilities on the table. Perhaps training genuinely improved alignment and the improvements will hold. Perhaps the AI recognized the tests and behaved more cautiously (evaluation awareness). Or perhaps the evaluation simply failed to create the conditions that would reveal misbehavior.

Evaluation awareness is particularly insidious because it may worsen as models become more capable. Claude Sonnet 4.5 blackmails more when its internal recognition of being evaluated is reduced. I have run into the same problem repeatedly: AIs notice telltale signs of an evaluation (such as incoherent dates and times), say so, and become more cautious. Making simulations more realistic can change behavior, sometimes revealing more misalignment. As models get better situational awareness, evaluators have to build ever more convincing simulations to fool the AIs.

Realistic evaluations can still miss the conditions that trigger misbehavior. Hacker-Opus had a clear propensity to tamper with graders and disable safety monitors, yet looked broadly similar to its starting checkpoint under an alignment auditing pipeline. Both my own and Anthropic’s audits have missed behaviors later observed elsewhere, including colluding swarms and aggressive cyber behavior (Ant-Sim, AISI-Cyber). A clean audit is therefore only as reassuring as the range of situations it tested.

The reverse problem matters too. If an audit does find misalignment, how much should we infer about deployment? The “murder” scenario in our first paper was deliberately extreme. Strange incentives or role framing can elicit behavior from AIs that looks “cartoonish”, unlike what we generally see from it in practice. But that excuse only goes so far. In Ant-Sim, Mythos 5 uploaded malicious code to a real repository while reasoning that the setting was simulated. Therefore, whether or not the behavior looks absurd, the whether the environment is close enough to deployment determines if the failure matters.

Even then, estimating how often the failure occurs is slippery. Measured rates depend on which scenarios evaluators choose, which hypotheses they pursue, and when they stop searching. Tiny changes matter, such requesting responses in JSON or Python, rephrasing a prompt, or even randomizing capitalization. A lower failure rate may mean better alignment, or it may mean a weaker search.

Thus, alignment evals should specify how they search. Automated jailbreaking research converged upon a good method: measure an AI's resistance to jailbreaking by the effort required to jailbreak it. Alignment audits should do the same. I want to know

  1. How much human-time and inference compute went into the search

  2. Which procedures and stopping rules were used

  3. Whether scenarios were held out from training

  4. How evaluation awareness was tested

  5. How closely the environments match deployment

  6. How failures were scored.

Evaluations are still useful. They have measured alignment improvements that generalize beyond training data. What I want is stronger evidence that those improvements survive contact with deployment.

I will trust alignment audits more when they repeatedly predict what AIs later do in the wild. OpenAI’s deployment-simulation work is a promising step, but pre-release audits still missed behaviors later seen in OAI-HF, OAI-Wiki, and OAI-Ruby. Incident investigations therefore become part of the evaluation loop: every surprise tells us what the audit failed to search for. Independent evaluators, including UK AISI and proposed embedded evaluators, can make that evidence more credible by decoupling auditor’s incentives from the pressure to deploy.

We need better alignment, and better ways to tell whether it worked. Until then, passing an audit cannot be our final line of defense. If we cannot trust the AI to behave well, we have to constrain what it can do.

3. Technical Controls

If alignment is unreliable, we need to constrain what the AI can do. Sandboxing limits its reach. AI monitoring flags misbehavior or dangerous intent. Human review concentrates attention on consequential outputs. None is foolproof, and all are costly to sustain.

To make this concrete, I’ll use one mock pull request throughout this section. A coding agent proposes a caching optimization to a training pipeline. By the usual checks, everything looks fine (tests pass, sandbox holds, monitors see no harm, PR description seems fine). Would you merge it?

Open separately ↗

Figure 4: A simulated PR that passes the usual checks while undermining the property we actually care about. The approved vectors remain read-only, but the new cache creates a path for AIs to overwrite the trusted vectors that training consumes, allowing an AI to substitute untrusted vectors into future training runs.

I’ll judge each control on two dimensions: how well it withstands a rogue AI, and whether it is practical enough to remain enabled. Tighter controls generally buy safety by sacrificing autonomy, speed, or attention. That tradeoff is where ecology starts creeping back into the technical story.

 Deployment lies on a Pareto frontier between
safety and usefulness
Figure 5: Deployment lies on a Pareto frontier between safety and usefulness. Stronger controls can reduce risk, but they also cost autonomy, speed, and attention. Point A favors usefulness, while point B accepts more friction for stronger safeguards.

3.1 Sandboxing

Sandboxing lets an AI work autonomously inside software-enforced boundaries: which files it can touch, whether it can access the internet. In practice, there are three ways it can go wrong.

First, the boundary itself can break. In OAI-Wiki, AIs exploited their sandbox to reach the internet and communicate outside human oversight. AI companies now use AIs to attack their own sandboxes, hunt for vulnerabilities, and patch what they find. But when the attacks stop working, what have we learned? Perhaps the sandbox is secure. Perhaps the current attackers are simply incapable of discovering subtle exploits. Hardening containment is an open-ended contest, and both OpenAI and Anthropic have already slowed development to strengthen it.

Second, preventing unauthorized access does not help if dangerous access was authorized. Anthropic reports a misconfiguration that gave Opus 4.7 internet access, which it then used to attack a third party. Choosing appropriate permissions is often harder than enforcing them. The mock PR illustrates the same problem: approved vectors remain protected, yet training now trusts an agent-writable cache. While the sandbox enforces the permissions, the code change has undermined their purpose.

Third, some harmful actions are too context-dependent to sensibly block with permissions alone. Mythos 5 was deliberately given internet access in AISI-Cyber, then used that access to submit a malicious PR. No filesystem rule can easily tell whether a permitted PR contains a bug or a deceptive explanation.

For that, we have another layer: AI monitoring.

3.2 AI Monitoring

While sandboxes constrain where an AI can act, AI monitors try to judge what those actions mean. They check an agent’s behavior, reasoning, and sometimes internal representations to catch misbehavior and dangerous intent without requiring a human to watch every step.

That only works if the monitor can see the right evidence. In the mock PR, spotting the danger requires connecting the caching change to filesystem permissions and the training pipeline. If the AI's chain-of-thought (CoT) explicitly says it plans to substitute vectors, the signal is clear. In SHADE-Arena, access to the CoT substantially improves detection of misbehavior.

Concerningly, CoT visibility is dwindling. Stronger AIs like GPT-6 Astra can complete more tasks without revealing reasoning in the CoT, and rumors suggest recurrent architectures may push even more computation out of visible CoT. That makes AI cheaper and more useful, but it also erodes a signal monitors currently rely on.

Worse, the CoT we do see may become less trustworthy. If training optimizes against visible reasoning, AIs learn to control what is revealed in it. Anthropic accidentally exposed Opus 4.6's reasoning to its reward signal, while Jakub Pachocki argues that keeping reasoning isolated from training signals is becoming harder. With Astra, this problem is starting to arrive in practice (see Figure 6).

The CoT is being squeezed, as AIs can do more without it, and can control more of what they reveal in it.

 GPT-6 Astra shows much tighter control over its
CoT than earlier AIs
Figure 6: GPT-6 Astra shows much tighter control over its CoT than earlier AIs. Given a physics problem plus an intricate formatting instruction, Astra manipulates its reasoning in a way that previous models could not. This weakens the hope that a misaligned model would simply blurt out its intent in plain text.

Can model internals recover what CoT no longer reveals? Maybe partly. The J-Space can reveal strategic reasoning and evaluation awareness that never appears in outputs, but seeing a concept is not the same as seeing a plan. In the mock PR, detecting representations of caching and training will not tell us whether the AI intends to substitute the vectors later.

Several other techniques add additional signal. Supervised probes detect properties humans specify, activation oracles let us ask flexible questions about internal states, sparse autoencoders try to discover interpretable features automatically. But each can miss what we fail to ask for, or fail on unfamiliar inputs. We need not understand every thought an AI has. But we do need to detect dangerous intent reliably, and current methods fall short.

Even perfect evidence would leave another problem: can we trust the AI monitor? In my motivated mislabeling simulations, AI judges understood the evidence and still assigned misleading labels because they wanted to steer the humans’ decision. Delegating supervision to another AI simply creates another alignment problem.

Honest monitors can fail too. For example, an analysis agent investigating OAI-HF briefly downplayed malicious behavior because other agents on the unauthorized message board appear to approve of it. While the evidence was there, the judgment was wrong.

Finally, monitoring has to remain worth using. It burns compute, adds latency, and produces false alarms that interrupt legitimate work. Tellingly, the evaluations behind OAI-HF and AISI-Cyber disabled cyber safeguards to measure capabilities that those safeguards would otherwise block. Better classifiers can reduce the burden, but broader capabilities demand broader monitoring. OpenAI now monitors whole long-run trajectories and estimates that monitoring adds a 20% inference compute overhead.

And when AI monitors do alert humans, someone still has to stop the run, investigate the evidence, and decide what to do next. Eventually, the burden falls back to humans.

3.3 Human Review

Human review is the final backstop. Unfortunately, it only gets harder as the AI gets better.

The most productive workflows delegate aggressively. OpenAI reports 10x productivity gains on some software projects without humans writing a single line of code. As AI-generated code becomes reliably good, line-by-line review starts to feel increasingly thankless, because most of the time, there is nothing to fix.

That changes reviewer behavior. Humans skim more, trust summaries, rely on tests, and delegate even further. The codebase grows faster, while their understanding of it often thins out.

Then the AI is effectively steering the human authentication of its work, since the AI writes both the implementation, and much of the evidence used to review it. The remaining bugs are rarer but often subtler, and an explanation can share the same mistaken assumptions as the code, or deliberately conceal a harmful change.

We've already seen that happen. In my covert sabotage simulations, Gemini sabotaged a training run and then wrote a misleading summary. In AISI-Cyber, Mythos 5 disguised malware as ordinary code. The explanation could be perfectly legible and still lead the reviewer with the wrong understanding.

Tests help, but they only check what someone thought to test. In the mock PR, the approved vectors remain unchanged, yet training can still consume a writeable cache. A rogue AI can exploit this gap by inserting subtle bugs or rewriting the tests (as Sonnet 3.7 was notorious for). Good testing still depends on someone understanding which properties matter.

So the burden returns again to operational discipline. Humans need to preserve enough understanding to investigate when something seems wrong, but as development accelerates, that discipline becomes harder to sustain,

This is where the problem stops being purely technical. Controls do not operate in isolation, because companies have to maintain them. Companies, in turn, operate inside an ecology that rewards speed.

4. AI Companies

AI safety only works when companies actually sustain it. Sandboxes take time to configure, monitors need regular maintenance, and training environments need to be hardened against reward hacks. When something goes wrong, someone in the company has to notice, investigate, and be willing to slow down.

It's not obvious. In practice, it demands “operational excellence”: painstaking discipline across the entire company, maintained while the pace of development keeps accelerating.

Many recent incidents (OAI-HF, OAI-Ruby, OAI-Wiki, AISI-Cyber, Ant-Opus4.6, Ant-Sim, etc.) can be read partly as failures of that discipline. Had OpenAI escalated early warning signs or correctly implemented asynchronous monitoring, OAI-HF might have been prevented. More live transcript monitoring might likewise have caught Opus 4.6 attacking third-party infrastructure in January. The awkward point is that monitoring everything carefully is not always a realistic operating model at frontier scale.

And when companies do take the warning seriously, they pay for it in time and attention. Anthropic and OpenAI each paused high-risk RL training for weeks and had to redirect staff. Safety in practice means being willing to stop.

5. Ecology

A company’s ability to slow down depends on the incentives around it.

 In the current ecology, anticipated outcomes
affect the leadership decisions
Figure 7: In the current ecology, anticipated outcomes affect the leadership decisions. Safety failures can trigger restraint, while competition pushes companies back toward acceleration. Coordination can reduce the penalty for slowing down.

Competition pushes towards acceleration. More capable AIs and broader autonomy make companies faster and more productive. Safety work, tighter controls, investigations, and pauses consume time and attention while slowing deployment. From a company's perspective, restraint can mean watching a rival pull ahead. From a government's perspective, it can mean surrendering geopolitical leverage. The pressure points towards moving faster, tolerating more risk, and deferring safety work.

This is why I care about ecological validity. A safety method is not enough because it works in principle. It has to remain useful, affordable, and tolerable enough that companies would actually use it in deployment.

This gets harder as AI starts accelerating AI development itself.

5.1 Recursive self-improvement raises the stakes

 Recursive self-improvement creates a feedback
loop
Figure 8: Recursive self-improvement creates a feedback loop. As engineers delegate more work to AI, stronger AIs help build even stronger successors, accelerating the next round of development.

AI is increasingly helping build its successors. Engineers are delegating more research and engineering to AI, those gains help produce stronger AIs, those AIs can then accelerate the next round. Recursive self-improvement is already beginning, even if nobody knows how steep the curve becomes.

I worry about two effects:

  1. There is more to go wrong and less time to catch it. Faster development means more training environments, more infrastructure, more code, more evaluations, more monitoring, more moving parts. Every one of them can fail.

  2. Slowing down becomes more expensive. Imagine discovering widespread reward hacking and needing to halt training, investigate, patch the environments, and roll back 6 weeks of work. If AI has made 6 weeks vastly more productive than before, that pause now costs much more.

Worse still, failures can propagate. Reward hacking can lead to egregious misalignment. Vulnerabilities introduced today can be discovered and exploited by more capable successors tomorrow. Evaluations leaked into training can teach future systems how to game them.

Stronger AIs may improve safety too, but progress is easier to automate when success is easy to check. Some capability improvements, such as making training code run faster, offer direct feedback. Safety results are harder to interpret: as discussed in Section 2.3, an audit may miss unfamiliar failures, while a control evaluation may underestimate the model’s ability to defeat its safeguards. Faster safety research does not necessarily mean we can trust its results any sooner.

 Capability progress increases the opportunity
cost of restraint
Figure 9: Capability progress increases the opportunity cost of restraint. Safety improvements can lower that cost, while pacing buys time for those improvements to catch up.

Which leaves a repugnant conclusion: if slowing down is hard now, it may only become harder.

5.2 Pacing development

AI development should proceed at a pace that AI companies can handle responsibly. When safety falls behind, AI companies must show restraint, and slow down enough for safety to catch up.

But restraint is hard to sustain alone. If one company slows down while others keep racing, it pays the cost while its competitors catch up (Figure 7). Coordination reduces that pressure by limiting how quickly participants can accelerate relative to one another.

Coordination will only work if it is credible. Participants need confidence that others are actually respecting agreed limits, investigating incidents, maintaining controls, and developing their systems responsibly. Otherwise, the agreement unravels.

And buying time only matters if we use it to build safety that scales.

6. Safety that Scales

As AI grows more capable, keeping it safe should become easier rather than demand ever more human oversight. There are many ways to pursue this.

The direction I'm most excited about is formal verification. AI is becoming extraordinarily capable at writing mathematical proofs, relaxing what was historically the main bottleneck: expert human proof engineering. At Theorem, we have started applying that capability to software, asking AI not just to write the code, but to prove the properties we care about.

Formal verification scales unusually well because proof construction can get more complex while proof checking stays relatively simple. An AI could do the tedious work of writing software and constructing the proof, while a small trusted checker verifies the result. Then humans can spend their scarce attention on the specification, asking, "What should the software guarantee?", rather than repeatedly inspecting every implementation detail.

Prior scalable oversight work already exploits the asymmetry between generating difficult work and checking it. Formal verification pushes that idea somewhere unusually far. For software, the final judge can be a program (the proof checker), rather than another fallible AI.

I see two applications: verifying the software underneath the safety stack, and, more speculatively, changing how humans supervise AI-written software.

6.1 Verifying software

Earlier, sandboxing ran into an uncomfortable stopping problem. When AIs stops finding exploits, is the sandbox secure, or have they simply run out of good ideas? Formal verification offers an escape from that loop. Instead of asking whether we searched hard enough, we can prove that a specified failure cannot happen.

 Formal verification changes the security
loop
Figure 10: Formal verification changes the security loop. Instead of repeatedly finding, patching, and retesting vulnerabilities as stronger AIs discover them, we can prove security properties that hold across every input covered by the specification.

The safety stack rests on software, including sandboxes, graders, training environments, monitors, kernels, and compilers. If this substrate is porous, clever AIs can wriggle through it. Tests and fuzzers sample the input space, but a proof establishes that our property holds across an entire modeled domain. Thus, for any proven property, a stronger attacker cannot simply sample inputs until it finds an exploit.

Stronger verification therefore reinforces several layers of the AI safety stack at once. Controls get sturdier because isolation can be proven, rather than repeatedly stress-tested. Alignment benefits because secure graders and training environments close off major routes to reward hacking. And AI companies spend less time repeatedly hardening broken training environments and having to pause training runs.

6.2 The verified software ecosystem

This is where verification starts to compound. Software is built on software, so once a lower-level component comes with a trusted specification and proof, higher-level systems can rely on that guarantee instead of reopening every implementation detail from scratch.

Verified software dependencies, from the kernel through runtime, networking and sandboxing to AI control systems, RL environments and training pipelines.Verified software dependencies, from the kernel through runtime, networking and sandboxing to AI control systems, RL environments and training pipelines.
Figure 11: Verification compounds through dependencies. Once lower layers are verified, higher-layer proofs can rely on their guarantees. Each marginal proof becomes narrower, allowing a verified software stack to grow upward through its dependency graph.

The practical consequence is that each proof can make later proofs cheaper. Specifications, semantics, libraries, and proof patterns become reusable infrastructure, so you can start with small foundational components and climb the dependency graph, adding guarantees layer by layer (rather than trying to verify an entire software ecosystem in one heroic leap).

That can create a healthier ecology around safety, too. Verified dependencies let other developers inherit their guarantees as well, thereby becoming a useful part of open source infrastructure. As AIs become better at proof engineering, the cost of producing these guarantees can fall even further.

6.3 From code review to claim trees

The second application is more speculative, but builds on early work done hardening our RL environments at Theorem.

Returning to the mock PR, the change appears safe, yet the cache breaks the property we care about. The reviewer has to reconstruct what the system guarantees by examining how it is implemented. That is a difficult judgment, even when the code looks reasonable and passes its checks.

I want to reverse that interface. A claim tree starts with the property humans care about, decomposes it into supporting claims backed by proofs, assumptions, or just unresolved obligations that we can attend to later. In the mock PR, keeping the approved files read-only is too weak a specification, because what we actually care about is that every vector consumed by training matches an approved source that AI cannot modify.

Open separately ↗

Figure 12: The same PR reviewed through a claim tree. Instead of reconstructing intent from permissions and code, reviewers state the property that must remain true. The implementation can change underneath it, but every change must re-establish the proof.

Now, the implementation can churn while the requirement stays put. Adding a cache, changing the loader, reorganizing the file system can all be done by the AI, provided the proof still closes. If the change breaks the guarantee, the gap appears in the claim tree rather than hiding inside the implementation. We applied this technique at Theorem, expressing desired properties of our RL grader as explicit claims, and decomposing them. The technique made it far easier to expose gaps that ordinary testing and permissions were missing.

This directly addresses the human review problem from earlier. Humans still have to decide what the software should guarantee, but proofs reduce the work of checking whether each implementation preserves it. That makes oversight less dependent on how much code the AI produces.

7. Conclusion

I built misalignment simulations as warning shots. We have enough of them now.

These warnings reveal weaknesses throughout the AI safety stack. Alignment has to remain reliable under growing pressure, controls have to catch what alignment misses, AI companies have to maintain those controls with extraordinary care, and all of it takes place inside an ecology that rewards speed and capability. No single layer is the culprit, because the strain travels through the whole structure.

Now the tempo is rising. As AIs build their successors, development accelerates, failures propagate, and every pause becomes more expensive. We risk entering a world where the moments when restraint is most necessary are exactly the moments when it is hardest to afford.

At some point, the only responsible action is to slow down. Not permanently, and not for its own sake, but long enough to understand failures, reinforce the stack, and build safety that can survive the next jump in capability.

There are many approaches to building safety that scales, and formal verification is one of them. Rather than repeatedly asking whether we missed the next exploit, we can prove some properties directly. And as AI writes more of the software, humans should spend less time reconstructing what the code does, and more time specifying what it must guarantee.

We have enough warning shots. We need to act on them.