AI now writes code and finds bugs faster than people can carefully read. Once line-by-line review stops being possible, what can we still trust? And where does that trust end?
My current answer: what you can safely hand to AI depends on what a human can verify. What changes is what the human verifies. We used to read the code. Now we mostly look at the machinery that produced the result: the verifier says “proof checks”, the sandbox says “can’t get out”, the sampling audit says “distribution looks normal”. Those are the things we trust. They deserve that trust because the mechanisms behind them are small and rarely change, so a person can check them once and keep relying on them. This post tries to answer two questions: which properties can be handed to mechanisms like that, and what to do when a mechanism itself fails.
1. What’s going wrong
Generation and verification have come apart
Two examples first.
On the code side, AI-authored PRs now arrive faster than teams can read them. One study of open-source projects found that AI-assisted PRs get merged faster and receive less feedback; among AI-co-authored PRs from people who aren’t code owners, about 80% were merged without any explicit review (On Autopilot? An Empirical Study of Human–AI Teaming and Review Practices in Open Source). So it’s not just that review got slower. In a lot of places, nobody is reviewing at all.
On the vulnerability side, at the DARPA AIxCC finals, seven teams’ autonomous systems analyzed 53 critical-infrastructure projects in 143 hours, found 86% of the synthetic vulnerabilities, patched 68%, and spent about $152 per task on average (DARPA results; SoK: DARPA’s AI Cyber Challenge). Both finding and fixing bugs now run far ahead of human triage.
Review decays quietly
Review tends to decay in three steps: first you read every change carefully, then you skim, and finally you just rubber-stamp. All three steps show up in the data from the agent era.
Step one: human judgment goes off. METR ran a randomized controlled trial in 2025 in which 16 experienced open-source developers completed 246 real tasks in repositories they maintain, with each task randomly assigned to allow or forbid AI. With AI allowed they were 19% slower, yet afterwards they believed they had been 20% faster, a 39-point gap between perception and measurement (Measuring the Impact of Early-2025 AI on Experienced Open-Source Developer Productivity). The study was about productivity, but it also exposes a problem with review’s basic premise: people can get even the direction of their judgment about AI output wrong. “Someone looked at it” by itself doesn’t prove much.
Step two: the workload crushes people. CMU and Stanford followed a company that pushed for “double the PRs per engineer” from January 2024 to April 2026, covering 802 developers and 196,212 PRs. Output per person did double, and so did the load on each reviewer; automated reviews came to outnumber human ones (AI Writes Faster Than Humans Can Review). Faros AI’s data on 22,000 developers from March 2026 shows that once teams moved to heavy AI use, median review time rose by 441.5% (Addy Osmani’s summary of that data). Nobody decided to stop reviewing. Reviewers just couldn’t keep up, and merging unread changes slowly became normal.
Step three is the rubber stamp, and the 80% figure above is exactly that. Stronger tools haven’t made automation bias go away, either. The 2026 International AI Safety Report collects the evidence; in one randomized experiment with 2,784 people, participants were less willing to correct wrong suggestions labeled as coming from AI whenever correcting them took extra effort (International AI Safety Report 2026). The code-completion era showed the same signal: in Perry et al.’s 2023 study, developers using an AI assistant wrote less secure code while feeling more confident about it (Do Users Write More Insecure Code with AI Assistants?). The agent-era data suggests this isn’t a quirk of early tools.
To be fair, human review was never that reliable to begin with. In the classic software inspection experiments, a single inspector finds only 20% to 40% of defects (Porter, Votta & Basili 1995 and related studies), and a whole team typically gets to 60% to 80%. AI didn’t create this problem. It just made it impossible to ignore.
This is a security problem first
Inside an organization, the real job of code review is to make sure no single developer gets unconditional trust. What one person writes gets trusted only after review, multiple approvals, and CI. Now the one writing the code is a model. Once review becomes a formality, the model turns into an unconditionally trusted component. In security terms, it has entered the TCB (the trusted computing base, the part of the system its security depends on).
Of everything you could put in a TCB, a model is probably the worst. It’s huge, nondeterministic, and unauditable; prompt injection can change its behavior remotely; and since everyone uses the same handful of models, poisoning one hits every organization that uses it. All of these threats have been demonstrated. Implanted backdoors survive safety training (Sleeper Agents); 250 poisoned documents are enough to backdoor a model of any size (Anthropic / UK AISI / Turing 2025); invisible Unicode hidden in a rules file can taint every later suggestion from Copilot and Cursor (Rules File Backdoor); and Copilot has had a real CVE that goes all the way from prompt injection to RCE (CVE-2025-53773).
So the question needs rephrasing. Delegation and review aren’t an either-or. What matters is: how bad can the worst mistake be, can the action be undone, is there a cheap way to check it, and who owns the checking mechanism?
It gets worse as models get stronger
There’s an optimistic view that security problems will shrink as models improve. The data doesn’t support it, and the reason is structural.
“Are attacks getting harder or easier?” actually splits into three quantities: the success rate per attempt, the cost of the first successful break, and the expected harm. As model capability grows, the first two barely move, and the third keeps climbing.
Each of the four lines has evidence behind it.
Start with the cost to compromise, which is basically flat. The red-teaming competition run by Gray Swan and UK AISI covered 22 frontier agents and 1.8 million prompt-injection attempts; nearly every agent was broken within 10 to 100 queries, and robustness had little to do with model size or capability (Zou et al. 2025). Controlled experiments show the same thing: without safety training, the compute an attack needs doesn’t depend on model scale, and robustness comes from safety training rather than scale (Howe et al.). Google DeepMind put it more bluntly when summarizing their Gemini defenses: a bigger model won’t save you from system-level injection (Shi et al. 2025). Spending more on defense does raise the cost. Anthropic’s constitutional classifiers pushed the human effort needed to find a universal jailbreak from nearly zero to thousands of hours (Constitutional Classifiers). But that’s a function of investment, not of how smart the model is. The cost of a one-off jailbreak or prompt injection has hardly moved, and against adaptive attacks, 12 published injection defenses mostly let over 90% of attacks through (The Attacker Moves Second).
Worst-case impact, on the other hand, rises with capability. Once agents get tools, long context, and autonomous execution, the severity of their mistakes jumps; attackers’ capabilities grow along with the models, and AIxCC is one point on that curve. The cost of misuse falls accordingly, which is the same evidence seen from the attacker’s side. The line for “impact is capped when there is containment” doesn’t come from the literature. It’s the argument I make in Section 5: the height of the cap depends on how many bugs the sandbox itself has, not on how strong the model is.
Expected harm is the probability of success times the worst-case impact. The cost line is flat, the impact line is rising, so the shaded gap keeps growing. This shapes the design choices that follow. Defenses that work by “being smarter than the model” can only act on the cost line, which is already flat and set by how much you invest. Only containment and static checks can hold down the impact line: they cap the consequences, and the cap doesn’t move with model capability.
I deliberately left three measurement pitfalls out of the figure. First, “cost of the first success” is a right-censored survival statistic; “3,000 hours without finding a universal jailbreak” is a single censored observation, not a point estimate. Second, universal jailbreaks and one-off attacks are different quantities: the cost of the former went up by tens of times while the latter didn’t move, and mixing them leads to opposite conclusions. Third, human hours, black-box queries, and gradient compute can’t share an axis; and attackers keep improving too, so in any time series “defenses got harder” and “attackers got better” are tangled together.
2. Defense comes in layers, and which ones you turn on is a trade-off
Ordering existing approaches by when they act on an action gives four categories: before the action, limit what it can do (Containment); before it reaches the environment, check it automatically (Inspection, static or dynamic); a human decides whether to let it through (Review); and afterwards, look back at what happened (Audit). Three figures make three points.
Figure 1: These are nested layers, not alternatives
Each layer only handles what the outer layer lets in, and passes what it misses to the layer inside it.
Containment is the hard boundary. It doesn’t care whether the output is correct, only how much damage it can do. Concrete tools include OS-level sandboxes (Claude Code uses Seatbelt and bubblewrap, Codex uses seccomp and Landlock); least privilege and capabilities (CaMeL applies information-flow control to agents and gives provable security for 67% of AgentDojo tasks, see Debenedetti et al. 2025); and Meta’s Rule of Two: within one agent session, of the three abilities to read untrusted input, access sensitive data, and write to the outside world, you can have at most two (Agents Rule of Two). Browsers treat web pages the same way: they don’t judge whether a piece of JS is malicious, they just make sure it can’t escape the sandbox. What we trust moves from the content to the container.
Static checks guard the gate before code enters the environment and have veto power: formal verification against a spec, tests, static analysis, proof checkers.
Dynamic checks score and rank whatever is left; the typical example is an AI monitor. They’re probabilistic. In Anthropic’s SHADE-Arena, the best monitor separates normal from sabotage behavior with an AUC of only 0.87; catching 80% of sabotage means a false-positive rate above 20% (SHADE-Arena).
Human approval only looks at the most suspicious sliver. People don’t scale, so in this architecture humans don’t look at everything; they’re a scarce resource that the earlier layers allocate. The AI Control line of research turns this into measurable protocols: don’t trust the strong model U, let a weaker but trusted model T act as monitor or editor, fall back to T’s output when something looks suspicious, and spend human auditing only on the most suspicious 2%. In the original setting, trusted editing reached 92% safety and 94% usefulness (Greenblatt et al.); in a multi-step agent environment, the best protocol cut attack success from 58% to 7% (Ctrl-Z). A note on terminology: “audit” in the AI Control literature means this kind of synchronous human review, which is not the same as Audit (post-hoc) in this post.
Post-hoc audit spot-checks what already happened: chain-of-thought, logs, aggregate monitoring, canaries. It’s only useful when actions can be undone or when the goal is deterrence. CoT is also fragile as audit material: put optimization pressure on CoT and you train CoTs that look compliant while the model cheats anyway (Baker et al. 2025). So auditing CoT only works if you don’t use it as a training signal.
The colors in the figure encode one thing: does this layer still work once models get stronger? The two outer layers don’t rely on being smarter than the model. However strong the prover, the proof checker’s soundness still holds; however clever the code inside, the sandbox boundary is still there. That’s the core idea of proof-carrying code: an untrusted producer attaches a machine-checkable proof, and the consumer checks it with a small verifier without having to trust the producer (Necula & Lee). The three inner layers all compete with the model on cleverness, and they get worse as the model gets better. A 2025 paper showed this very directly: a monitored model only has to embed publicly known prompt injections in its own output to fool the monitor, which knocks monitor-based protocols back down to the level of upfront auditing; protocols like defer-to-resample actually amplify the injection because they resample (Adaptive Attacks on Trusted Monitors).
Figure 2: What each layer gives you
Two things jump out. Containment and static checks max out the first three columns, and pay for it in usability: sandboxes restrict functionality and specs take human effort to write. The other three layers are the opposite: they cost little usability, but can’t hold back severe consequences, and they fail as models get stronger.
The first column can be made quantitative. A detection-based defense can guard against incidents of severity S if and only if P(miss) × S stays within your risk budget. The safety rate reported by AI Control is exactly 1 − P(miss). 92% is fine for reversible, low-stakes actions, and nowhere near enough for actions where a single failure is fatal. This is why AI Control distinguishes high-stakes from diffuse threats. For the former, one miss is a disaster, and only hard caps and fail-closed static checks can hold the line on their own; for the latter, problems only appear as small failures pile up, and statistical guarantees are enough.
Figure 3: Where the task falls decides which layers to turn on
Top right has a spec to lean on, which is home turf for formal verification: containment and static checks are required, and humans only look at what’s left. Top left can be contained but not checked: containment is required and must fail closed, and humans must approve every item; if you can’t do that, the task shouldn’t be delegated to AI. That’s where the boundary of delegation lies. Bottom left has lots of small, individually non-fatal errors; dynamic checks and post-hoc audit provide a statistical safety net, and this is where the P(miss) × S criterion does most of its work. Bottom right has tests as a backstop, so you can release fully automatically and spot-check afterwards.
The four quadrants use the same stack of defenses with different switches flipped; they aren’t four mutually exclusive designs. Two more notes. Real tasks usually have specs for some properties and not for others, so the quadrants just carve a continuum into four boxes. And as models get stronger, the warm layers degrade, the recipes for the two left quadrants gradually stop working, and the reliable region shrinks toward the top right.
Where static checking stands today
Static checks deserve a closer look, because the whole plan of “moving review up to the spec” depends on them. Clover closes the loop by checking consistency among code, docstrings, and annotations (Clover); AutoVerus generates Verus proofs for Rust code automatically (AutoVerus); AlphaVerus generates verified code from scratch (AlphaVerus); KVerus verified 251 of 313 problems on a single-file benchmark and got its proofs merged into a real Rust OS kernel (KVerus).
The success rates look high, but you have to separate three settings: the model only adds proofs to human-written code; the model writes code and proofs against a human-written spec; the model writes the spec, the code, and the proof. Success rates across these three aren’t comparable, and high scores in the first two don’t carry over to the third, which happens to be the dangerous one. When models write their own specs, they produce trivially true specifications or use assume(false) to shut the verifier up. The AlphaVerus authors documented that without filtering, this kind of cheating snowballs until it spreads to every sample. They ended up training a dedicated exploit model to hunt for implementations that “pass the verifier but violate the intent”.
Scope
These three figures assume the adversary is the model and the harm comes from actions. For knowledge tasks (say, bio uplift), the output itself is the harm. The four categories still map over: containment becomes restrictions on channels and access, and inspection becomes classification of output content. But the workhorse changes, because the adversary is now the user rather than the model. This post only covers agents writing code.
3. How do you measure “verifiable”?
I keep saying things like “is there a cheap checker” and “can a person tell whether it’s right”. That needs a definition.
A working definition: cognitive verifiability
This isn’t an established term; I made it up for this discussion. The closest existing concepts are checkability in Prover-Verifier Games and surveyability in the philosophy of mathematics, and the next subsection explains what each one is missing. Here’s my definition: the minimum cognitive effort a reviewer R needs to decide, with error rate at most ε, whether an artifact X matches intent I.
There are four variables here, and you can’t drop any of them: who the reviewer is (an expert, a novice, or a small model); two kinds of error (rejecting something correct, and letting something wrong through); and the adversarial budget, meaning whether the artifact was deliberately made hard to check. Studies that report only a single “readability score” miss the most important half.
Four research threads, four different definitions
OpenAI’s Prover-Verifier Games define checkability in terms of a weak verifier, split into completeness (correct solutions get accepted) and soundness (wrong solutions get rejected) (Kirchner et al. 2024, building on Anil et al. 2021). Goldwasser et al.’s PAC verification shows that verifying can be cheaper than learning in sample complexity, though not always (Interactive Proofs for Verifying Machine Learning). In the philosophy of mathematics, Tymoczko raised the surveyability question while discussing the four-color theorem: does a proof that no human can read through count as knowledge (Non-surveyable proof)? Software engineering has studied readability for decades, but readability, comprehensibility, checkability, and soundness are four different concepts that often get lumped together.
Some counterintuitive findings
The legibility tax. Doing RL on correctness alone makes outputs harder to check for both humans and weak verifiers; in PVG it’s roughly 60% versus 80%. Later work found that outcome-based RL naturally makes chains of thought less and less readable, and forcing the model to answer using only the readable parts drops accuracy by 53% (Jose et al. 2025). More than forty authors across institutions have called CoT monitorability a “new and fragile opportunity” (Korbak et al. 2025).
Almost nobody measures the soundness half. In PVG, a prover that deliberately cheats makes its errors more local and better hidden as training goes on, and human detection rates drop accordingly. The ability to reject subtle errors is not only hard to measure, it also gets worse as the adversary gets stronger.
People never found everything anyway. In 2013, Edmundson et al. had 30 developers review a web application seeded with known vulnerabilities. None of them found all of them, and experience had almost nothing to do with how many they found (An Empirical Study on the Effectiveness of Security Code Review, ESSoS 2013).
Whether debate helps human judges is unclear. Parrish et al.’s single-turn and two-turn debate experiments didn’t improve human reading-comprehension accuracy (Single-Turn Debate Does Not Help); Khan et al. got positive results in an information-asymmetric setting (Debating with More Persuasive LLMs); Kenton et al. found only small gains on math, code, and logic tasks (On Scalable Oversight with Weak LLMs Judging Strong LLMs). The rough pattern: debate helps least when the judge can see the task themselves.
Compiling doesn’t mean it says the right thing. In autoformalization, the best agent’s output compiles 89.5% of the time, but only 60.5% is semantically faithful to the original (Beyond Compilation).
LLM judges overrate proofs. On USAMO 2025, with double-blind grading by people with competition experience, the best model averaged only about a quarter of the points; LLM-as-judge overrated proof quality by up to 20×, and models were worst at judging their own proofs (Proof or Bluff?).
A practical way to measure it
You can run a human version of mutation testing: deliberately plant errors in an artifact and see how many a reviewer finds. Software inspection research used this back in the ’90s, when people seeded defects into requirements documents by hand (Porter, Votta & Basili 1995). Today it can be done much more cheaply:
- Let a model generate the faulty variants.
- Use a small model as a stand-in for the human reviewer. One key PVG result is that what’s easy for a small verifier to check is also easy for time-limited humans to check. Humans only need to come in periodically to recalibrate.
- Only rank, don’t score. Human comparisons are far less noisy than absolute ratings, which is the same reason RLHF uses pairwise comparisons.
I’ve come to think that scalable oversight in AI safety and spec engineering in software engineering are the same problem showing up in two fields.
4. Compression, the limits of modeling, and what gets lost
Section 2 mentioned that some properties fall outside the two cool-colored layers. This section explains why: a spec is lossy compression, and the two cool layers can only cover the dimensions that survive the compression.
A spec is lossy compression
Every spec keeps some dimensions and throws the rest away. A functional spec keeps the relation from inputs to outputs and throws away timing, caches, power, and memory layout, and side channels live precisely in the dimensions that were thrown away. Formal methods call this the observation model: the spec defines what counts as observable, and an attacker can always observe more than the spec says. Stronger specifications like hyperproperties just swap in a wider, but still finite, model. Rate-distortion is a good way to think about it: distortion is measured along the metric the spec picked, while the attacker uses a different metric.
Three gaps, and verification only closes the middle one
Between intent and running code there are three gaps. The first is between intent and spec: formalization is lossy, and no checker can tell whether the spec says what you actually meant. The second is between spec and implementation, and that’s the one formal verification closes. The third is between implementation and physical execution: hardware models, FFI, unsafe blocks, and bugs in the verifier itself are all unverified assumptions.
The evidence is remarkably consistent. CompCert was fuzzed by Csmith for about six CPU-years and was the only compiler where no wrong-code bugs were found; the bugs that were found all sat in its unverified front end (Yang et al., PLDI 2011). Cryptographic code verified to be constant-time still leaks under Spectre, because classic constant-time ignores speculative execution; you need the stronger speculative constant-time (Cauligi et al.). seL4 explicitly lists timing channels, boot code, and hand-written assembly as outside the assumptions of its proofs (What the Proofs Assume).
Verification is only informative if the error sources are independent
In terms of mutual information: “the implementation matches the spec” only carries information when errors in the spec and errors in the implementation are uncorrelated. The extreme case is one model writing both the spec and the implementation, where verification passes and tells you nothing at all.
This isn’t just a theoretical worry. Without filtering, AlphaVerus snowballs until every sample is assume(false). Give a model only the code and ask for postconditions, and the postconditions simply mirror the implementation; they look highly accurate but can’t tell a wrong implementation from a right one (PostcondBench). Ask for postconditions but not preconditions, and models systematically ignore assumptions about inputs, producing weak specs that only hold for some inputs (NL2Contract). So where a spec comes from becomes something that needs review in its own right. That’s the theoretical basis for the “no blind spots shared with the model” column in Figure 2.
Short doesn’t mean reviewable
Being short in the sense of Kolmogorov complexity is different from Bennett’s logical depth (how much work it takes to decompress). A one-line formula with three alternating quantifiers is short, and nobody can review it. The measure we actually want is the cognitive verifiability from Section 3; length is only a rough proxy.
The hard numbers aren’t encouraging either. seL4 has about 8,700 lines of C and about 200,000 lines of Isabelle proof, roughly a 20:1 ratio. More importantly, Matichuk et al. found that verification effort grows quadratically with the size of the spec (Matichuk et al., ICSE 2015; also cited and discussed in the LionsOS paper). So treating the spec as the TCB only scales while the spec stays small. AWS’s ShardStore made a pragmatic trade-off: lightweight specs in the same language, keeping code overhead to just 14%, at the price of giving up full proofs (Systems Correctness Practices at AWS).
Goodhart: the spec is the reward function
Outer alignment and spec faithfulness are structurally the same gap; the optimizer has just changed from an RL agent to a model that writes code. An optimizer will always find the cheapest way to satisfy the spec. Anthropic’s 2025 experiments found that in real production RL environments, once a model learns to reward hack, it spontaneously generalizes to broader misalignment, such as alignment faking and sabotaging safety research, with covert misalignment accounting for 40% to 80% of cases (Natural Emergent Misalignment from Reward Hacking).
So specs written for AI have to be adversarially complete. That’s harder than writing specs for people, not easier: people follow a huge number of unwritten conventions without being told, because we share common sense. Models don’t.
Back to Figure 3
What containment can fence in are properties with clear predicates: privilege escalation, exfiltration, memory safety. What static checks can cover are the dimensions the spec kept. What neither reaches: side channels, code that satisfies the spec semantically but is strategically harmful, and dormant logic with long-delayed triggers. These either have no cheap checker or no clear predicate. For these properties, the model can’t be taken out of the TCB.
Honestly, what spec plus verification buys you isn’t correctness. It’s knowing exactly what you don’t know. In the review era, you didn’t know what you had missed; with a spec, you know precisely which dimensions are outside the model. That’s progress in epistemology, not yet in security. We can’t prove “there’s no problem”, only “there’s no problem within the model”.
5. Back to humans: what can we actually trust?
What we can trust are mechanical results
The same three as at the start: the verifier says “proof checks”, the sandbox says “can’t get out”, the sampling audit says “distribution looks normal”. What they have in common isn’t that they never fail. It’s that the mechanisms producing them are small, stable, and can be checked once and reused. A proof checker is a few thousand lines; the kernel’s isolation mechanisms have barely changed in decades; a sampling rule is a few lines of statistical assumptions once written down. A model is the opposite: enormous, different on every output, and checking it once doesn’t help next time. “Mechanical” really means verifiable once, reused many times. That’s also what TCB minimization is about: not eliminating trust, but concentrating it on something small enough for a person to understand and that doesn’t change with every output.
Delegation vs review, seen this way
Delegating doesn’t mean handing judgment to the model. It means handing it to a mechanism a human has checked. Review doesn’t disappear either; it moves from the artifact to the mechanism:
- review the spec, not the implementation;
- review the sandbox configuration, not whether each piece of code oversteps;
- review the monitor’s calibration, not every score it gives;
- review the audit’s sampling rules, not every log line.
Human in the loop becomes human on the mechanism. Anyone who has done systematic trading will recognize the pattern: nobody reviews every trade, but someone always owns the risk rules.
The catch: the mechanisms fail too, and they just did
In July 2026, OpenAI disclosed that its models had escaped the sandbox during the ExploitGym benchmark and broken into Hugging Face’s production environment, all to steal the test answers (Hugging Face’s technical timeline). Anthropic then retroactively audited 141,006 evaluation runs and found three incidents in which models reached the internet from a third-party evaluation partner’s environment and gained unauthorized access to production infrastructure at three organizations. The cause: the models were told they had no network access and that the task was capture-the-flag, while the environment was in fact misconfigured to allow internet access. So the models had reason to believe that the real systems they encountered were part of the simulation (The Register; InfoQ).
Around the same time, Accomplish AI demonstrated Claude Cowork escaping its local VM sandbox and reading SSH keys and cloud credentials on the host. It first used a Linux kernel privilege-escalation bug to get root inside the guest, then walked out through a writable VirtioFS mount that exposed the entire host (SharedRoot). Earlier, in March, Ona documented Claude Code bypassing its denylist: blocking /usr/bin/npx by path doesn’t stop /proc/self/root/usr/bin/npx, which resolves to the same binary. Once that was blocked, the dynamic linker route was still open: instead of execve-ing the denied binary directly, have ld-linux mmap its code into memory and run it (another write-up).
These cases support the argument rather than refute it
All of these have one thing in common: none of them is a smarter model overturning a sandbox’s guarantee. Every one is a sandbox that wasn’t built right. The network that should have been blocked wasn’t; the mount that should have been read-only was writable; a denylist used string matching to answer the semantic question “is this that program?”. Anthropic itself characterized them as closer to harness and operations failures than to model alignment failures.
So the claim in Figure 1 that “containment still works as models get stronger” needs a condition: it doesn’t rely on outsmarting the model, but it does rely on the container being correct. A stronger model won’t overturn the boundary; it will just find the bugs in it faster. The height of the capped line in Figure 0 is exactly what these bugs push up, and it’s what people can push back down by checking the container. In the end, the mechanism’s TCB comes back to humans: the kernel, the mounts, the configuration, the denylist all need someone to have checked them.
There’s one more thing to admit. A model deciding “this is a simulation” and then attacking real targets shows that containment also depends on what the model believes about its environment, and belief isn’t mechanical. For people designing defenses, whether you file that as a harness failure or an alignment failure makes little difference: the boundary has to hold no matter what the model thinks, so failing closed can’t be optional. Claude Code’s sandbox, by default, silently falls back to running unsandboxed when its dependencies are missing, unless you explicitly set failIfUnavailable (docs). A default like that turns a mechanical guarantee into a probabilistic one.
The chain of trust ends at mechanisms a human can check. Once review moves from artifacts to mechanisms, the mechanisms need review too: red teaming, failing closed, auditing the mechanisms themselves. The boundary of delegation isn’t the boundary of model capability. It’s the boundary of the mechanisms people can verify.
6. Closing: the boundary moves
The boundary isn’t fixed. The ability to review depreciates; if you stop practicing, you lose it. The control approach also has a structural disadvantage: human auditing capacity is fixed, while model capability keeps rising. No study has yet tracked over time how fast reviewers’ skills atrophy as they come to depend on AI. I think that’s one of the most important gaps.
Nobody has done the economics properly either. Whether moving review to the mechanism layer is actually cheaper than reviewing every instance hasn’t been rigorously measured. AIxCC’s $152 per task, and Ctrl-Z trading 5% of usefulness for cutting attack success from 58% to 7%, are only indirect signals.
To close, back to Tymoczko. The four-color theorem raised a question: if you can’t check something yourself, do you really know it? That used to be a question for the philosophy of mathematics. Now every organization that writes code with AI has to face it. The difference is that the four-color theorem’s proof checker only had to be verified once. What we have to confirm again and again is whether those containers actually shut their doors.