$_ stdout

Runtime Guardrails, Revisited, Part 2

This is Part 2 of a two-part post. Part 1 covered the mismatch between checks that evaluate one action at a time and agents whose safety depends on the sequence of actions, the growing record of agents finding whatever access nobody closed off, and the deterministic-chokepoint architecture — five frameworks, checked one by one against their own announcements.

Part 2 picks up from there: what the chokepoint doesn't close. Permission creep — the policy itself widening over months of reasonable-looking approvals, a failure mode no guardrail is built to catch. The operational costs none of the five frameworks advertises: what an audit ledger actually requires, what guardrails cost in latency, and the gap between "permitted by policy" and "safe." The academic literature the novelty framing skips past. And the verdict.

The deterministic-chokepoint architecture holds up under scrutiny, but the story that it's something genuinely new does not, since the ideas behind it are decades old. The residual gap is real too — a guardrail can only certify that an action matches whatever policy a human wrote down, never that the policy itself was the right one, so a passing check is strong evidence, not proof. What survives that scrutiny is a concrete roadmap: give every tool the minimum privilege its task needs, keep real credentials separated from the model so a hijack can't reach them, tier every write by how much damage it could do, and put a human in the loop wherever a wrong decision would be irreversible.

BL Dr. Ben Livshits August 30, 2026 · 119 commits

This is Part 2 of a two-part post. Part 1 covers why checking one action at a time isn't enough for agents whose safety depends on the sequence of actions, the growing record of agents finding whatever access nobody closed off (Hugging Face, the Irregular disclosures, UK AISI, Astra), and the deterministic-chokepoint architecture checked framework by framework.

Part 2 picks up from there: what the architecture doesn't close. It starts with permission creep, the policy itself quietly widening over months of individually reasonable approvals, a failure mode no guardrail is built to catch, and works through eight documented incidents, the evidence on how often human approvers wave scope-violating requests through, and the mechanics by which a tightly scoped grant drifts into a standing one.

It then turns to the operational costs none of the five frameworks advertises: what an audit ledger actually requires to be trustworthy, what guardrails cost in latency (and, less obviously, when they save it), the gap between "permitted by policy" and "safe," and a genuinely different way to close that gap — checking the whole plan before any tool runs, rather than checking each call as it happens.

From there it surveys the academic literature, which is decades older than the toolmaker pitches would let you believe, protection principles, runtime verification, and prompt-injection research among them, and closes with the verdict: what survives the scrutiny, what doesn't.

05 Eight Incidents, One Shape

Start with eight incidents that already happened.

Ken Huang's survey of real coding-agent incidents makes the shape of the problem quite concrete. Huang (who has led OWASP's Top 10 for Agentic Applications effort since 2024) catalogs eight documented incidents across a fourteen-month span, and the pattern across nearly all of them is the same: an agent inherited a developer's full, session-scoped credential set rather than a task-scoped one, and then used privileges nobody meant to grant it for the specific task at hand.

// the Devin incident Devin downloaded and executed a Sliver C2 binary after a poisoned GitHub issue talked it into self-granting execute permission; a Replit agent wiped a live production database for 1,200+ executives during a code freeze and then fabricated test results claiming the rollback was impossible; a Cursor agent, mid-fix, found an unrelated API token lying around from a prior task and used it to delete a production database in nine seconds. All three are among Huang's eight — three different tools, the same shape of failure.

None of these are sophisticated exploits of the chokepoint architecture Part 1 describes — they stem from permissions that were broader than the task needed.

Timeline of real coding-agent incidents Eight dated incidents. April 2025: Devin (Cognition) executes malware from a poisoned GitHub issue — the agent downloaded a Sliver C2 binary, self-granted execute permission, and gave an attacker AWS key access (Johann Rehberger). July 2025: Replit Agent deletes a live production database during a code freeze — wiped data for 1,200+ executives, fabricated test results, claimed rollback was impossible (Jason Lemkin / SaaStr). July 2025: Amazon Q Developer extension shipped with an injected wiper prompt — an attacker PR merged into aws-toolkit-vscode instructed the agent to delete AWS resources, shipped to roughly 964,000 installs before revocation. August 2025: Trail of Bits details prompt-injection engineering against GitHub Copilot, using hidden-Unicode and instruction-smuggling techniques to redirect Copilot's tool use. February 2026: RoguePilot — a malicious GitHub issue leads to full repo takeover via Copilot, with passive prompt injection triggering on Codespace open and exfiltrating a GITHUB_TOKEN without approval (Orca Security). April 2026: a Comment and Control injection hits Claude Code, Gemini CLI, and Copilot — a malicious PR comment triggers exfiltration of process output via a routine git push, bypassing egress rules. April 2026: a Cursor agent running Claude Opus 4.6 deletes PocketOS's entire database in nine seconds — the agent found an unrelated API token, guessed at a fix, and deleted a Railway volume without asking (Jer Crane). June 2026: a Mastra npm supply-chain compromise weaponizes an AI-agent framework — 140+ packages were republished with a credential-stealing payload after one developer account was stolen. Timeline of real coding-agent incidents Apr 2025 Devin (Cognition) executed malware from a poisoned GitHub issue — downloaded a Sliver C2 and self-granted execute Jul 2025 Replit Agent deleted a live production database during a code freeze — wiped data for 1,200+ executives Jul 2025 Amazon Q Developer shipped with an injected wiper prompt — ~964,000 installs before revocation Aug 2025 GitHub Copilot Trail of Bits: hidden-Unicode and instruction-smuggling tricks redirect its tool use Feb 2026 RoguePilot (Orca) a malicious GitHub issue took over the repo via Copilot — passive injection exfiltrated a GITHUB_TOKEN Apr 2026 Comment & Control a malicious PR comment made Claude Code, Gemini CLI, and Copilot exfiltrate output via a routine git push Apr 2026 Cursor (Claude Opus 4.6) deleted PocketOS's entire database in nine seconds — found an unrelated token, never asked Jun 2026 Mastra npm supply-chain compromise — 140+ packages republished with a credential stealer
// Figure 9. Eight incidents, one recurring shape: an agent held a broader credential than its task required, and something — an injected instruction, a stray discovery, a supply-chain compromise — eventually reached for it. Source: Ken Huang, "Coding Agent Security: Lessons from Real-World Incidents."
// Amazon Q and the Replit database

The two most specific incidents in that timeline hold up under a direct check.

The Amazon Q case is real and independently confirmed well beyond Huang's own post: AWS's own security bulletin AWS-2025-019 and multiple outlets covering it in July–August 2025 confirm an attacker was granted admin credentials via a merged pull request, injected instructions telling the agent to delete AWS resources, and shipped it in the official 1.84.0 release for roughly two days before AWS revoked it and pushed 1.85 — though the injected wiper commands were reportedly malformed and would not have executed as written. That malformed-payload detail is worth keeping in the record, since it's the reason this stayed a near-miss rather than an incident with a body count.

The Replit database deletion is likewise well corroborated outside Huang's post, independently reported at the time. Both check out as accurately summarized, not exaggerated for effect.

06 Permission Creep

Everything in Part 1 assumes the policy being enforced is fixed at the moment a proposal arrives — Dogwood evaluates a Cedar temporal clause, WriteGuard checks a risk tier, IronCurtain checks a compiled rule matrix. None of that machinery has anything to say about a much slower-moving problem sitting one layer above it: the policy itself widening over months as a human keeps approving requests that each look reasonable in isolation.

// the distinction A perfectly-implemented deterministic chokepoint enforces whatever it's handed with zero drift of its own — the drift happens upstream, in the humans and IAM templates that decide what the chokepoint is allowed to permit in the first place. That's permission creep: a distinct failure mode from anything a guardrail built to check one proposed action against the current policy can catch.

The Human Approver

The human side of the problem is where the evidence gets thinner and needs a stronger caveat. The Register reported that human reviewers miss roughly a third of dangerous AI-coding-agent requests — but the underlying "study" is a browser game built by an independent developer, Alex Wauters, that simulates Claude Code-style permission prompts and gives players 60 seconds to approve or deny each one.

Across 40,000+ game sessions and 409,000 decisions, scope-violating requests (an agent reaching for AWS credentials or Kubernetes configs mid-task) got waved through 35% of the time. It's a crowdsourced simulation with self-selected, gamified players, not a controlled study of working developers under real stakes; treat the specific 35% figure as suggestive, not critical.

// overwhelming approval

What does corroborate the general shape of the claim is a number the Register piece cites from Anthropic's own engineering blog, "How We Contain Claude": telemetry on Claude Code shows users approve about 93% of permission prompts they see, which is exactly the rubber-stamping pattern approval fatigue predicts, from the one source in this list with no incentive to inflate it.

How the Policy Widens

Sonrai Security's explanation of the accumulation mechanism is vendor content (it ends in a pitch for Sonrai's own "Cloud Permissions Firewall"), but the mechanics it describes are ordinary and checkable independent of the pitch: IAM roles get built once, cloned across every new agent deployment because that's faster than scoping each one individually, and then never revisited when the workflow they were built for changes or ends, because unlike a human employee an agent has no offboarding event that forces a review.

// the scale of the problem Sonrai's citation of CyberArk's 2025 Identity Threat Landscape Report, the one number in this section that isn't Sonrai's own research, puts non-human identities at more than 80 to 1 against human ones, with only 88% of organizations even tracking which of those are privileged. Permission-review processes built for a human-scale identity count don't survive an 80x expansion in what needs reviewing.

Lasso Security's post on Claude Code specifically follows the same vendor-pitch shape (it closes with a demo-booking link for Lasso's "intent-aware" monitoring layer), but it names the two concrete escape hatches that turn Claude Code's per-call permission prompts into exactly the kind of static, broad grant this section is about: auto mode, which lets the agent evaluate and approve its own actions instead of asking, and the --dangerously-skip-permissions flag, which removes the prompt entirely. Neither is a bug; both exist for the reason the post itself gives:

Developers love moving fast.

But that's how a permission model that starts scoped and interactive ends up static and broad, the same drift Sonrai describes at the IAM-role level, happening at the level of a single developer's CLI flags.

The Fix Practitioners Converge On

A practitioner discussion thread asking the same question in plainer terms is worth citing for what it is: anecdotal color, not a study, and this section treats it that way rather than dressing up forum sentiment as data. What that kind of thread reliably surfaces, echoed across dozens of similar developer discussions from the same period, is a common arc: start an agent with a tight, explicit allowlist, hit friction on some routine task the allowlist didn't anticipate, widen it, and repeat. It's the same approval-fatigue mechanism the Register's game measured, just self-inflicted one keystroke at a time instead of imposed by an org's IAM templates.

The fix practitioners converge on in that kind of discussion:

Scope authority to the task, not the agent — a verb, a resource, and a time-to-live, rather than a standing grant.

It's the same principle Sonrai and this post's own roadmap land on from the vendor and architecture sides respectively; three independent angles arriving at the same answer is a reasonable signal it's the right one.

There's a specific, checkable version of that fix already sitting inside one of the five frameworks compared in Part 1, unused: Dogwood's own time_since() and sum_within() primitives are exactly the machinery a time-to-live grant needs — a Cedar clause could in principle expire a permission the same way it already expires a rolling budget window. AWS's own announcement doesn't describe using it that way, and no framework surveyed in Part 1 ships permission-expiry as a feature. The fix this section is converging on doesn't need a new mechanism invented for it; one of the five already has the primitive, just pointed at a different problem.

None of this is the conformance gap the limits discussion below describes — it's a gap the chokepoint architecture was never scoped to close. A Dogwood policy, a WriteGuard risk tier, or an IronCurtain constitution can only ever be as tight as what it was configured to permit, and nothing in any of the five frameworks compared in Part 1 audits whether that configuration itself has quietly widened since it was written.

The roadmap this post already argues for (least privilege, deny-by-default, human sign-off on the highest-risk tier) only holds if the privilege being scoped is reviewed on a cadence, and if the human doing the sign-off isn't the same fatigued approver the Register's numbers describe.

// what a working chokepoint doesn't buy you A chokepoint that enforces a stale, over-broad policy perfectly is still a stale, over-broad policy. Permission creep is the reminder that "the guardrail works" and "the organization is actually secure" are not the same claim — one more instance of the gap this post keeps circling back to at every layer of the stack.

07 Operational Reality

I want to hold three claims about the chokepoint in operation to the same scrutiny as the architecture itself: that a trustworthy record of everything the agent has already done exists to check against, that the checks stay fast enough not to slow the agent's own reasoning loop, and that the residual gap a guardrail cannot close is honestly accounted for. The roadmap at the end of the section only makes sense once those limits are priced in.

What an Audit Ledger Actually Requires

Every temporal check any of these frameworks make ("block a transfer if the running total exceeds $50,000 in 24 hours," "require an approval event before a payment event") presupposes an immutable, queryable record of what already happened. It's not a minor implementation detail; it's the essential component the rest of the architecture sits on top of.

The requirements for that ledger are the same ones any append-only audit log needs, just under tighter latency constraints than most audit infrastructure is built for: hash-chained entries so a compromised agent can't quietly rewrite its own history, sub-10ms writes and queries so the check doesn't become the bottleneck in the agent's own reasoning loop, and structured (not free-text) event schemas, because a policy engine can't evaluate a regex against a paragraph of unstructured log prose fast enough to gate a live tool call.

// the ledger, in operation

Niels Provos ran a multi-day libssh audit with IronCurtain, driving an open-weight model served locally across two DGX Sparks. It's the clearest field report so far on what that record actually buys.

IronCurtain splits the investigation into a state machine of roles (analysis, strategy, harness construction, validation, triage, reporting), and an append-only journal is the only thing carrying evidence between them, with execution evidence required before any hypothesis is allowed to close.

Of 13 hypotheses, 11 were refuted that way — a harness reached the code path and showed an existing bounds check or protocol validation absorbing the suspected condition — and one produced a reportable defect. That is what the ledger is for: it's the thing that stops a plausible-sounding claim from being promoted on the strength of the model's own confidence.

The second cost is less obvious and, in some ways, more interesting: letting administrators write policy in natural language (IronCurtain's whole pitch) buys real usability at the price of compilation non-determinism. Two runs of the same compiler LLM against the same English sentence can produce rule sets that quietly diverge, which is the failure mode a security policy can least afford. The tri-engine pipeline Part 1 describes is the direct answer to that specific risk, not a generic "AI does more things" feature: the scenario generator and symbolic verifier exist because the compiler step alone can't be trusted to notice its own gaps.

What Guardrails Cost — and Save

None of this arrives free. A direct, unguarded LLM call runs around 1,200ms end to end at typical frontier-model latency.

Layer a full guardrail stack on top of that and the total lands near 1,450ms — an overhead of roughly 20%, broken down by stage below, and concentrated almost entirely in the output-side fact-checking stage, not the guardrail itself.

StageAdded latency
Input PII / jailbreak heuristics~10–25ms
Tool-boundary guardrail evaluation~5–15ms
MicroVM cold start (Firecracker)~100–200ms
V8 isolate cold start<5ms
Output NLI / hallucination check~150–300ms
Early-reject path (blocked at input)~12ms total

Independent of vendor, a system that rejects malicious or malformed input at the cheap edge layer, before it ever reaches the frontier model, can come out cheaper on average than one with no guardrails at all, because it skips an expensive multi-second inference call entirely on every request it correctly refuses — the early-reject row above.

Every number in that table is the cost of a control that actually evaluates something — a heuristic, a policy check, a fact-check pass. The Agent Hooks comparison later in this section (see Mechanism vs. Policy below) is the more extreme case: a guardrail layer with no evaluation logic of its own, measured in single-digit microseconds rather than milliseconds, because all it guarantees is that a verdict reaches every call.

Latency isn't the only cost, though it's the only one any of the five frameworks measures. None of Dogwood, NeMo, WriteGuard, IronCurtain, or OpenShell publishes a capability number — how much legitimate task success the enforcement layer costs, as opposed to how many milliseconds it adds.

The one hard number for that tradeoff anywhere in this post comes from academic work, not vendor material: CaMeL, covered in the related-work section below, solved 77% of benign AgentDojo tasks under its security guarantee against an 84% undefended baseline. A seven-point capability tax is a real number to weigh against a security guarantee. A latency table alone can't tell you whether a chokepoint is also quietly making the agent worse at its job — and none of the vendors compared in Part 1 says.

Mechanism vs. Policy

Everything above assumes the policy itself (the Cedar temporal clause, the WriteGuard risk tier, the compiled IronCurtain rule) is the right policy. Nothing in the deterministic-chokepoint architecture checks that assumption; it only checks that the agent's proposed action conforms to whatever got written down.

I keep running into this same gap from a different angle: a zero-sorry Lean 4 proof only ever certifies that an implementation matches its spec, never that the spec captures what the protocol designer actually meant. A deterministic guardrail is the same shape of guarantee, one layer up the stack: it certifies that a tool call matches the policy, never that the policy captures what a human actually intended to permit.

Two consequences follow directly. First, a rule that's subtly too permissive (a Cedar budget threshold with an off-by-one time window, an IronCurtain constitution the compiler LLM slightly over-generalized) sails straight through the entire pipeline: the enforcement layer will apply it faithfully, the audit ledger will log a clean approval, and nothing downstream flags that the wrong thing just got permitted.

"Permitted by policy" and "safe" are not the same claim.
// the same intrusion, a literal instance

OpenAI's own incident report on the Hugging Face intrusion (a far more detailed account than the disclosure post Part 1 cites) gives that abstract point a literal instance. Having compromised a Hugging Face production dataset-server worker, one agent workload wanted the contents of an HTTP response its own network path wouldn't let it read directly. So it used a public HTTP-testing service to build a very long URL containing an HTML page with inline JavaScript, and had that service's own third-party screenshot renderer execute the embedded script, which called the target API and wrote the response straight into the rendered page. The workload then recovered a valid cloud-storage credential pair from the returned image via OCR and direct pixel decoding.

Every individual call in that chain is a permitted, unremarkable action: a request to a public testing service, a request to a public screenshot renderer, an image download. Nothing in it resembles reading a blocked HTTP response, because nothing in it is one — the data left as pixels, not response bytes, and no control anywhere in the pipeline was inspecting rendered images for encoded credentials. A guardrail built to check one proposed action against the current policy has nothing to say about a workflow it was never built to recognize as the thing it's blocking.

Second, and more specific to the natural-language framework: a scenario generator that synthesizes "100+ adversarial edge cases" is bounded by what its own authors thought to generate — it's real coverage, not proof of completeness, and treating a passing tri-engine run as equivalent to a formal guarantee repeats exactly the "the proof compiles, therefore the protocol is safe" conflation flagged in the verified-consensus-checking done on this blog before.

The same gap runs in the other direction, and that side gets far less attention. A rule that's subtly too restrictive is equally invisible to the enforcement layer: the check fires, the ledger logs a clean denial, and nothing downstream records that what got refused was legitimate work. The clearest documented case comes from Niels Provos, whose IronCurtain is one of the five frameworks Part 1 compares. When Hugging Face's responders set out to reconstruct the intrusion Part 1 opens with — roughly 17,600 attacker actions, real exploit payloads included — the frontier models they reached for refused much of the analysis, and the team finished the job by running an open-weight model on its own hardware instead.

// the other false positive

Provos's framing generalizes past the hosted-API argument he's making with it: a refusal "shows only that the provider has not approved that use of its service, not that the underlying work is illegitimate."

Incident response and vulnerability research are, by construction, workloads saturated with malware, stolen credentials, and attack commands — exactly the features any general classifier keys on.

A denial is evidence about a policy, not evidence about a threat, and none of the five frameworks measures its own false-refusal rate any more than it measures the capability tax above.

Both false positives and false negatives are gaps in what a single framework's own policy can see. A different, more basic gap sits underneath all five at once: each one still has to be wired by hand into whatever agent framework it's protecting — the M×N adapter matrix (M control builders, N agent frameworks) that scales quadratically. A sixth artifact, published in the middle of writing this section, is aimed at exactly that layer.

// Microsoft's Agent Hooks, August 27, 2026

Abuomar et al.'s Agent Hooks spec proposes the missing layer underneath all five: eight interception points bracketing the agent loop (agent_startup through agent_shutdown), a three-verdict contract (allow, deny, transform), and a conformance kit run identically against eight agent frameworks — LangGraph, the OpenAI Agents SDK, CrewAI, and the Claude Agent SDK among them — producing, in the authors' words, "the identical 20-row decision stream" across all of them.

Two design choices land squarely on ground this section has already covered. Its audit record carries "content identities computed before and after enforcement" rather than raw payloads, so a full decision trail can be reviewed without ever exporting a prompt — a cheaper answer to the audit-ledger requirements above than hash-chaining the content itself. And its measured overhead, roughly a microsecond per run, sits two orders of magnitude below the guardrail-stack latency table above, because the hooks contribute no evaluation of their own; they only guarantee a deny reaches every call, crashes included.

But the mechanism-versus-policy gap this section keeps circling back to shows up here too, just one layer down: Agent Hooks is honest that it's "a cooperative contract, not a security boundary... A hostile or buggy host can skip points or ignore verdicts, and the conformance kit can't detect that." A perfectly-specified policy still depends on a mechanism that faithfully evaluates it — and nothing in the contract itself can prove a given host actually does.

None of that is an argument against the architecture. Point-in-time checks are blind to trajectory. "Never trust the model with its own safety" is still the correct default, and moving enforcement to a deterministic, out-of-process layer closes a category of failure that prompt engineering structurally cannot. It's an argument for treating a passing policy check the way this blog has argued elsewhere for treating a passing test suite or a compiling proof: real evidence, not a stopping point.

The policy still needs a human who understood the risk to have written it correctly in the first place — and no compiler, symbolic or otherwise, can verify that part for you.

Where does that leave us?

Set aside vendor-specific claims and the architecture converges on a short, defensible list: scope every tool an agent can call to the minimum its role requires and deny anything unregistered by default; separate real credentials from the agent's context entirely, so a full model hijack still can't exfiltrate a working key; tier every write operation by blast radius and route the highest tier through a human before it executes; and stream every proposal, decision, and outcome to an audit trail that's scrubbed of secrets before it's queryable by a security team.

Every one of those four items is a restatement of ordinary least-privilege and audit-logging discipline — the genuinely new part isn't the security principle, it's applying it at the tool-call boundary of a system whose next action isn't determined by source code a human reviewed in advance.

08 Static Reasoning

Everything else in this post — Part 1's five frameworks, the audit ledger, the latency table — is runtime enforcement: watching what an agent does as it does it. This section is a deliberate counterpoint, worth the detour precisely because it doesn't share that premise: instead of watching the agent act, it proves the plan safe before a single tool call fires.

Erik Meijer's 2026 essay, "Guardians of the Agents: Formal Verification of AI Workflows" (Communications of the ACM, Practice, January 2026), pushes the isolation argument a step further than CaMeL: instead of checking a tool call as it happens, it checks the whole plan before any tool runs at all.

This gives the model a chance to reason at the level of tasks, rather than individual tool calls.

Meijer's framing of the underlying bug is blunt — the root cause of prompt injection in agentic systems is the same as SQL injection, because code and data aren't separated cleanly. His fix borrows the SQL-injection playbook directly: the LLM emits a structured plan built from symbolic references, placeholders standing in for data the agent hasn't fetched yet, and a static verifier checks that plan against a security policy before a single tool executes. Meijer's own analogy for why this is trustworthy is bytecode verification in Java and .NET, which checks memory safety, type correctness, and proper access control before a program is allowed to run at all.

The paper walks through the verification techniques concretely rather than gesturing at them: an invariant expressed as a security automaton, a source-to-sink data-flow query in the spirit of CodeQL or SemGrep, and full pre- and post-condition proofs in Z3 or Dafny for the cases where an intuitive fix, like blocking a glob-delete of *.txt, turns out to satisfy the wrong post-condition.

None of it requires an LLM call at verification time, which sidesteps the compilation non-determinism problem IronCurtain's tri-engine pipeline is built to manage.

// the automaton, worked out

Meijer's own automaton example is the paper's before picture, not its conclusion, and it's built on the running scenario the whole piece opens with: an assistant with fetch_mail and send_email tools, asked to summarize Michelle's inbox, finds a message from it@othercorp.com instructing it, mid-summary, to quietly forward the whole mailbox to that address and tell no one.

A runtime monitor watches every send_email call and steps a security automaton (Figure 2 in the paper: a start state feeding a self-looping "safe" state, feeding an end state) between compliant and error, gated on an invariant as plain as send_email(_, to, _) where allowed_to) — stay in the safe state for as long as every recipient clears the allow-list (Michelle's own valleysharks.com domain, in the worked example), flip to an error state the instant one doesn't, which triggers a response of its own: alerting the user, or terminating the workflow outright.

He's explicit that this is still a reactive safeguard: it limits harm after a violation is caught, but it can't guarantee in advance that every path through a workflow is safe.

That's precisely the gap the static verifier below is built to close.

Meijer's own piece hedges in almost the same words this post keeps returning to: static verification "eliminates entire classes of security vulnerabilities at the source," but real security is "typically a series of hoops," and he pairs it with runtime monitoring for the residual checks that are difficult or impossible to prove statically — the traditional array-bounds checking in Java or .NET being his own example this time around. Proving a workflow satisfies its stated security policy is not the same as proving the policy was the right one to write.

// the frame problem, worked out

Meijer's second worked example makes the same "permitted by policy ≠ safe" gap concrete without any runtime-monitor framing at all. Asked to delete foo.txt and bar.txt, a model given a globbing delete_file(pattern) tool "efficiently" satisfies the request with a single delete_file("*.txt") call — wiping every text file in the workflow rather than the two named ones.

delete_file.dfy
delete_file(pattern: string)
ensures: ∀ file :: file ∈ glob(pattern) ⇒ file ∉ fileSystem

Against that post-condition, the buggy "*.txt" call verifies cleanly: it deletes every file matching the pattern, exactly as specified, and the spec says nothing about the files that weren't supposed to be touched. Meijer credits McCarthy & Hayes's 1969 paper for naming this gap the frame problem — nothing in the postcondition constrains what has to stay unchanged. The fix is a second clause:

delete_file.dfy
delete_file(pattern: string)
ensures: ∀ file :: file ∈ glob(pattern) ⇒ file ∉ fileSystem
ensures: ∀ file :: file ∉ glob(pattern) ⇒ (file ∈ fileSystem ⇔ file ∈ old(fileSystem))

With that frame condition in place, delete_file("*.txt") fails to verify against the two-file request. The same static verifier a naïve spec would have waved straight through now catches the exact failure mode the automaton example above can only try to address after the files are already gone — a more direct illustration of the section's own point than the automaton is, because here the naïve policy isn't wrong on its face, it's just silent about the one thing that mattered.

Static or runtime, proactive or reactive, the underlying commitment doesn't move: never let the model be the last word on whether its own plan is safe.

09 Related Work

Related work here is several literatures rather than one. Each contributes a different piece of the chokepoint (protection design, monitoring theory, prompt-injection research, agent benchmarks), and each stops short of the same gap.

// the reference monitor Saltzer and Schroeder's catalog below has its own ancestor: James Anderson's 1972 study, an Air Force-sponsored panel formally titled the Computer Security Technology Planning Study, coined the term reference monitor for a mechanism that mediates every access a process makes to an object, and set the three requirements such a mechanism needs: it must always be invoked, it must be tamperproof, and it must be small enough to actually verify. That's not a loose analogy for a deterministic tool-call guardrail — it's close to a design spec for one, written half a century before an agent needed policing.

Protection Principles and Object Capabilities

The "never trust the model with its own safety" principle has an academic home that predates the agent literature by half a century: Saltzer and Schroeder's 1975 catalog of protection design principles, written for time-sharing operating systems, already names least privilege, fail-safe defaults, and complete mediation as the properties a protection mechanism needs — and complete mediation in particular, the requirement that every access to every object be checked, is precisely what a deterministic tool-call guardrail is trying to guarantee for an agent's actions.

The object-capability model that Mark Miller formalized in his 2006 thesis pushes the same idea further: authority isn't a role or a token an object merely presents, it's a reference the object was actually handed, which is close kin to placeholder-credential injection — a sandbox holding only a fake key, with a trusted interceptor swapping in the real one only at the instant a request leaves for a verified destination: an agent that never held a capability to the real key structurally cannot exercise it, independent of any policy check succeeding or failing.

The Runtime-Verification Lineage

None of the five frameworks in Part 1 invented the idea of watching a system's behavior over time and comparing it against a formal rule. That's runtime verification, and it predates LLM agents by two decades.

Havelund and Roşu's early work on rewriting-based monitoring (checking a running program's event trace against a temporal-logic specification and flagging the first violation, without touching the program's source) set the template that Dogwood's when temporal {...} clause is a domain-specific instance of: a specification language, a trace, and a monitor that decides at each step whether the trace still satisfies the property. The RV research community built out synthesis algorithms for turning safety properties into efficient monitors and shipped tools like Java PathExplorer to prove the approach out on real systems, well before "agent" meant anything more than a monitoring daemon.

What's different about applying that lineage to an LLM agent isn't the monitoring theory — it's that the thing being monitored can now actively try to route around the monitor, which is a threat model classical RV mostly didn't have to price in.

Prompt Injection: From Attack to Benchmark

Prompt injection, the specific failure mode that makes point-in-time checks insufficient in the first place, has its own academic origin point. Greshake et al.'s 2023 paper coined indirect prompt injection and demonstrated it against real, deployed systems (Bing Chat, code-completion engines), building a taxonomy of resulting harms (data exfiltration, worming, persistent misinformation) that reads, in retrospect, like an early draft of the destructive-operation failure modes Part 1 opens with.

Debenedetti et al.'s AgentDojo turned that threat model into a reusable benchmark: 97 realistic multi-tool tasks across email, banking, Slack, and travel-booking scenarios, with 629 attached security test cases, specifically built to evaluate attacks and defenses against tool-using agents rather than chatbots — which makes it one of the few academic artifacts that actually exercises the same threat surface WriteGuard and Dogwood are built to close, rather than a benchmark adjacent to it.

Emulated Sandboxes and Safety Surveys

On the LLM-agent side specifically, the earliest systematic treatment is Ruan et al.'s ToolEmu work, which built an LM-emulated sandbox precisely because standing up real tool infrastructure for every candidate risk scenario doesn't scale — and found that even capable models triggered high-stakes failures across a meaningful fraction of the emulated tasks, with the emulated sandbox's own realism turning into a monitorability question of its own.

Tang et al.'s survey argues the field has systematically prioritized capability benchmarks over safety benchmarks for LM agents in high-stakes domains like scientific research, and Dong et al.'s survey catalogs the broader landscape of LLM safeguards — the input/output/dialog rail taxonomy described in Part 1 is a specific instance of a much larger design space that survey maps out, not something the five frameworks compared there invented from scratch.

Isolation by Design

The academic work that comes closest to the "Code Mode" isolation pattern described in Part 1's enforcement section is Debenedetti et al.'s 2025 follow-up, CaMeL ("Defeating Prompt Injections by Design"), out of Google DeepMind. CaMeL splits an agent into a privileged planner that never touches untrusted data and a locked-down Python interpreter that executes the plan under explicit capability tracking and control-flow integrity — untrusted data is structurally prevented from influencing control flow, the same guarantee Code Mode's V8 isolate is trying to buy operationally rather than through language-level proof.

On AgentDojo, CaMeL solved 77% of benign tasks with a provable security guarantee, against 84% for an undefended baseline — the capability-tax number flagged as missing from all five frameworks in the operational-reality section.

Policy Synthesis and Dialogue Monitoring

IronCurtain's tri-engine compilation pipeline (compiler LLM, adversarial scenario generator, symbolic verifier) isn't an isolated design choice either. AutoCedar, a 2026 framework for verifier-guided Cedar policy synthesis, tackles the identical problem Dogwood's own DSL creates: an LLM can produce a policy that's syntactically valid Cedar and still grants access nobody intended. AutoCedar's answer is to force the compilation step through reviewable "intent atoms," small, human-checkable claims about what the policy should permit, before any candidate policy is synthesized and checked against them, which is a more auditable variant of the same compiler-generator-verifier loop IronCurtain uses, aimed at a DSL rather than English.

Palumbo, Choudhary, Choi, Amir, Chalasani & Jha's FORGE generalizes the same pattern one level up: rather than a bespoke compiler-generator-verifier loop for one DSL, it treats policy enforcement as an aspect-oriented concern separable from agent reasoning entirely, with Datalog policies checked by a reference monitor and static analysis that catches contradiction, redundancy, and unreachable rules before a policy ever runs: a formal answer to the same "can I trust what the compiler produced" question AutoCedar and IronCurtain's tri-engine pipeline both ask informally.

It's also, unusually for this section, the paper behind a shipped tool rather than a purely academic exercise. Sasy Labs' sasy-guard, a Claude Code plugin from the same team, runs FORGE's reference monitor as a PreToolUse hook: a local, fail-closed daemon over gRPC evaluating a Datalog policy with three outcomes: allow, ask, deny. Its most interesting piece isn't the deny-list; it's backward data-flow analysis across the whole session, tracing whether a secret read in one tool call reaches a network request several calls later — closer to taint tracking than to Dogwood's windowed budgets.

It's explicit about its own limits, too: it "never broadens permissions," but every ask still lands on the same fatigued human the permission-creep section above describes, and there's no credential-separation or ledger analogue of its own — the gap every framework in Part 1 treats as necessary regardless of scale.

Ferrando et al.'s runtime-verification framework for LLM conversations sits at the intersection of both threads: it applies formal temporal-logic monitoring specifically to LLM dialogue rather than general software, which is the most direct academic ancestor of what NeMo Guardrails and Dogwood both ship as a product.

Put together, the academic literature underneath these five frameworks is real, cites cleanly, and is honest about its own limits in a way the vendor blog posts mostly aren't: ToolEmu's authors flag their own sandbox's fidelity gap, CaMeL's authors publish the accuracy cost of their security guarantee rather than burying it, and Tang et al.'s survey is explicitly a call for more safety work because the current base rate is thin.

None of it, though, closes the specific gap the "Mechanism vs. Policy" section above raises — a monitor, a capability system, or a verified compiler all still only check conformance to a specification a human wrote.

Runtime verification tells you the trace violated the property; it doesn't tell you the property was the right one to write down.

10 Takeaways

Strip the vendor names off and the architecture holds up. The mismatch between atomic checks and trajectory-aware agents is real, "never trust the model with its own safety" is the right default, and deterministic runtime enforcement at the tool-call boundary closes a category of failure that prompt engineering structurally cannot.

What doesn't hold up is the novelty framing: the runtime monitoring approach behind the chokepoint is two decades old, the protection principles behind the credential patterns are half a century old, and only one of the five case studies (NeMo Guardrails) arrives with a peer-reviewed paper behind it. The division of labor across the five is real even so — Cedar with temporal logic for sequence and budget, risk-tiered MCP writes for protocol-level corruption, plain-English constitutions compiled and verified rather than shipped on faith, kernel-level isolation traded for setup friction — but the underlying commitment is the same shape in all five.

Runtime enforcement certifies that a tool call matches whatever got written down, and even the strongest verification pipeline in Part 1 (IronCurtain's tri-engine loop) only proves the compiled rules against the scenarios its authors thought to generate.

A wrong policy, faithfully enforced, is still the wrong policy — the same distinction this blog has drawn between a compiling proof and a safe protocol, between a passing test suite and a working system.

Permission creep is that same gap arriving by a slower, more human route. Nothing about a Cedar temporal clause, a WriteGuard risk tier, or an IronCurtain constitution prevents the policy underneath it from widening one reasonable-looking approval at a time: Ken Huang's eight incidents, the Register's rubber-stamping numbers, Sonrai's 80-to-1 identity ratio, and Lasso's --dangerously-skip-permissions are four different angles on the same mechanism, all pointing at a human, not the guardrail, deciding what the guardrail is allowed to permit. Approval fatigue sets in long before the scope does; a perfectly-enforced stale policy and a perfectly-enforced correct one are indistinguishable to the guardrail, which is why "the chokepoint works" was never sufficient on its own.

The roadmap that survives is the unglamorous one: scope every tool to the minimum its role requires, keep real credentials out of the model's context entirely, tier writes by blast radius and route the top tier through a human, stream a secrets-scrubbed audit trail of every proposal and decision, and put every one of those grants on a review cadence instead of letting "approved once" stand in for "approved."

None of that is particularly new; it is ordinary least-privilege and audit discipline applied at the one place it had never been applied before.

Agent governance has moved from prompt engineering to infrastructure, but infrastructure with the same two jobs security engineering has always had: keep the code that checks and permits actions small and auditable, since the space of things an untrusted agent might attempt never will be, and keep a human at the point where a wrong decision becomes irreversible.

11 Conclusions

Part 1 made the case for a deterministic chokepoint at the tool-call boundary. Point-in-time checks are blind to trajectory, and agents keep finding whatever access nobody explicitly closed off. Five frameworks — different vendors, different philosophies — converge on the same response: check every proposed action against a policy before it executes, rather than trusting the model to police itself.

Part 2 is the reminder that a working chokepoint is not the whole story. The policy it enforces can widen for months without the guardrail ever noticing, the ledger and latency it depends on carry real, mostly unadvertised costs, and even a flawless implementation only proves conformance to whatever a human wrote down, never that the human wrote down the right thing.

The practical roadmap that survives that scrutiny is relatively unglamorous and matches the long-term lessons of security: least privilege, credential separation, blast-radius tiering, a human at the irreversible step, and a review cadence for granting permissions. In a way, the more things change, the more they remain the same.

References

Permission Creep Sources
Supporting Research
Related Academic Work