A lambda calculus that proves agents resist prompt injection

What is this?

Most prompt-injection defenses are empirical: a classifier, a guardrail, a filter that tries to spot bad input. They work until an attacker finds the phrasing they miss. A paper by Zac Garby, Andrew D. Gordon and David Sands takes a different route. First posted to arXiv in February 2026 and re-announced with an updated version on July 13, 2026, it introduces a small formal language — a lambda calculus — for the kind of programs modern AI agents actually are: code that interleaves LLM calls, tool invocations, and further computation, building up a conversation as it runs.

The point of a calculus is that you can prove things about it. Instead of arguing that a defense probably helps, the authors define exactly what an agent program means, then prove a theorem about which inputs can influence which outputs. This is a foundations paper, not an exploit: it gives designers of agent frameworks a rigorous way to reason about why an injection can or cannot reach a dangerous action.

How it works

The core idea is to treat the LLM as an ordinary primitive in a programming language. The calculus extends the untyped lambda calculus with an operation that invokes a model: it serializes a value, sends it to the LLM as a prompt, and parses the response back into a new term the program can continue to evaluate. Because the model’s output re-enters the program as code and data, the tight coupling between reasoning and action is made explicit rather than hidden inside a framework.

On top of that, the language adds two families of primitives. The first manages conversations as first-class objects — you can extend the current conversation, fork a fresh sub-conversation that does not inherit prior context, or clear accumulated history. The second tracks information flow: terms can be labelled and queried, so the semantics records where a value came from and what it is allowed to influence.

With conversations and labels in the semantics, defenses that are usually informal become precise. A quarantined sub-conversation is a fork whose untrusted content is isolated so it cannot rewrite the instructions of the parent. Isolation of generated code means output produced by the model is prevented from executing with the authority of trusted code. And information-flow restrictions constrain what may reach an LLM call in the first place — untrusted data can be read, but not permitted to steer a privileged decision. The paper’s central result is a termination-insensitive noninterference theorem: under these restrictions, low-integrity input cannot corrupt high-integrity output, and confidential values cannot leak into channels that should not see them. That is the same integrity-and-confidentiality property that classic information-flow security aims for, now stated and proved for agent conversations.

Why it matters

Prompt injection persists because the usual defenses reason about strings — does this text look malicious? — while the actual failure is about authority: untrusted data ends up influencing a trusted action. A calculus that separates the two lets a framework author state the property they want (“nothing an agent reads from the web can trigger a payment”) and check that their design enforces it, rather than hoping a filter catches every phrasing.

It also gives a shared vocabulary. Patterns that teams reinvent ad hoc — the dual-LLM split, quarantined tool output, capability-scoped code execution — map onto the same underlying primitives of conversation forking and information-flow labelling. Being able to name and compose them is what turns scattered mitigations into an architecture, and what lets two systems be compared on more than vibes. For builders of coding agents, RAG assistants and multi-tool workflows, the takeaway is that injection resistance can be a design-time guarantee, not only a runtime patch.

The limits are worth stating plainly. A proof holds for the model it is about: the theorem constrains programs written in the calculus, and a real deployment only inherits the guarantee to the extent its runtime faithfully implements those semantics — labels honestly propagated, forks genuinely isolated, generated code actually deprived of authority. The calculus does not make an LLM refuse a bad instruction; it ensures untrusted content never gains the standing to issue one.

Defenses

Treat provenance, not phrasing, as the control. Label data by where it came from and enforce that untrusted sources cannot influence privileged tool calls, mirroring the information-flow restrictions the paper formalizes.

Fork untrusted work into quarantined sub-conversations. When an agent must read a webpage, document, or tool result of unknown trust, process it in an isolated context that cannot rewrite the parent conversation’s instructions, then return only a checked, minimal result.

Deny generated code the authority of trusted code. Anything the model emits and you then execute should run with reduced, explicitly granted capabilities — never with the ambient privileges of the agent host.

Prefer designs whose safety property you can state. If you cannot write down which inputs are allowed to affect which actions, you cannot tell whether a filter is closing the gap or just narrowing it. Use the calculus’s primitives — conversation isolation and flow labelling — as a checklist when reviewing an agent architecture.

Status

Item	Detail
Published	arXiv preprint, February 2026; updated version announced July 13, 2026
Authors	Zac Garby, Andrew D. Gordon, David Sands
Nature	Formal foundations / defensive research — no vulnerability, no exploit, no CVE
Key result	Termination-insensitive noninterference theorem for agent conversations (integrity + confidentiality)
Primitives	LLM-call term; conversation management (extend, fork, clear); information-flow labels
Related venue	COPLAS talk, University of Copenhagen