The LLMbda Calculus reframes agent confidentiality as a property you can prove rather than one you prompt-engineer. Updated to v2 on July 10, 2026, the paper casts LLM agent conversations, tool calls, and retrieved context as a call-by-value lambda calculus in which every value carries a security label propagated through every reduction. The payoff is a noninterference theorem: an attacker-controlled input cannot change what a trusted output reveals.
How does the calculus track information flow?
LLMbda is an untyped call-by-value lambda calculus extended with first-class constructs for agent behaviour, and it enforces confidentiality by attaching a label to every value and propagating that label through every reduction step. According to the paper, the added constructs are prompt-response conversations that can be forked and cleared, code generation, and dynamic information-flow control. A label travels with its value; reductions combine labels so that an output’s label reflects the join of every input that touched it. Provenance-based defence against prompt injection becomes expressible and provably sound, and the calculus does not commit to a specific architecture: the guarantee is a property of the language, not of a particular wiring of planner and executor models.
Forking and clearing conversations matter because multi-session agents are where leakage actually bites. A secret surfaced in one conversation reaching an output in another is the failure mode runtime filters are worst at catching, and in LLMbda these operations are part of the labelled reduction rather than escape hatches around it.
How is this different from the dual-LLM pattern?
The leading proposed defences hard-wire isolation into the architecture and then apply policy checks at the boundaries; LLMbda instead makes information flow a first-class, tracked property of the language itself. The paper gives three reasons current defences are hard to trust: runtime flow tracking is error-prone, deliberate relaxations of the policy are hard to audit, and the dual-LLM pattern is baked into the architecture rather than expressed in the semantics. CaMeL’s separate control and data channels confine by construction. LLMbda confines by proof. The difference matters when someone relaxes a rule to ship a feature: in an architecture-bound design the relaxation lives in application code the security argument never sees, whereas in a calculus with labelled values the relaxation is a reduction the theorem has to account for.
Can it prove a secret cannot leak between conversations?
Within the model, yes. The central result is a termination-insensitive probabilistic noninterference theorem over the entire calculus, including the code-generating agents, with an insulated variant that holds even when the attacker chooses every untrusted input. Noninterference is the property that an observer who controls the untrusted inputs learns nothing about the secret-valued inputs beyond what the policy explicitly permits. In LLMbda that means a secret surfaced in one forked conversation cannot reach an output in another, because the labels on the secret-bearing values prevent the reduction that would emit them into a lower-labelled context. Clearing a conversation is a real operation in the calculus, not a hope that the model forgets.
The insulated variant is the stronger claim: noninterference holds even when the attacker supplies every untrusted input. In an agent that means retrieved documents, tool outputs, and anything else the model can be coaxed into reading are all hostile. That is the threat model prompt injection actually presents, not a curated set of adversarial prompts.
Two caveats the paper is honest about. The theorem is termination-insensitive, so it says nothing about what an attacker might learn from whether a computation halts. It is also probabilistic and scoped to the calculus’s treatment of the model as a labelled function, which sets aside the question of whether the model itself is a side channel.
What did the AgentDojo benchmark show?
On 1,296 attacked runs of the AgentDojo banking benchmark, the paper reports, an LLMbda-built agent with enforcement always on matched the utility of CaMeL run without policy checks, while resisting all but two attacks. The utility comparison does the heavy lifting. The paper reports that the policy checks CaMeL relies on cut utility in half, so the secure configuration of the dual-LLM defence costs half the task success rate. LLMbda with enforcement permanently on held utility at the un-checked CaMeL baseline and still blocked all but two attacks.
| CaMeL (dual-LLM) | LLMbda | |
|---|---|---|
| Where isolation lives | Architecture: separate control and data channels | Language semantics: labelled values |
| Enforcement | Policy checks at boundaries | Label propagation, always on |
| Utility on AgentDojo banking | Policy checks halve utility; without them, baseline | Matches CaMeL without policy checks |
For a builder, the trade is the point: confidentiality that does not tax the agent’s usefulness, rather than confidentiality bought by gutting what the agent can do. The two successful attacks are worth naming as a limitation rather than buried. The paper does not claim the calculus is attack-proof; it claims a proved property and then shows the property holds up empirically with a small, known residual.
Why does a Lean-verified interpreter matter?
The reference interpreter is implemented and verified in Lean, and the paper describes it as the first LLM agent harness whose executable is itself the subject of machine-checked security theorems. This is the detail that separates LLMbda from formal-methods theatre. The usual failure mode is a paper that proves a property of an idealised calculus and then ships an unverified Python harness that calls the model, leaving the theorem and the running code in different rooms. Here the verified artefact is the harness: the executable that issues prompts and consumes responses is the thing the Lean proof covers. The noninterference theorem is not about a cleaned-up model of the agent; it is about the agent that runs.
What does this mean for “secure agent” claims?
Once noninterference is the bar, most vendor claims about secure agents reduce to sandboxing, which is a strictly weaker property: it confines where code runs, not what information reaches where. Sandboxing stops an agent from writing to the filesystem or calling a blocked API. It does not stop a prompt-injected agent from folding a secret from retrieved context into a response the sandbox is only too happy to emit, because emitting a response is an allowed action.
The deeper move is that a four-decade formal-methods lineage finally has a concrete target in LLM agents. Dorothy Denning’s lattice model of secure information flow and the noninterference property Goguen and Meseguer defined in 1982 have spent forty years as the reference vocabulary for secure systems that almost nobody ships. LLMbda instantiates that vocabulary against the thing the industry is actually building. The bar it raises is specific: a secure agent is one whose confidentiality rests on a theorem you can name, not a filter you hope holds.
Will this ship in production agent stacks?
Not soon, and the paper does not claim it will. Shipping agent stacks carry no such discipline: they are Python and TypeScript orchestration over model APIs, with provenance tracked, if at all, in ad-hoc string metadata that nothing enforces. The gap between the isolation vendors imply and what their designs can actually prove is exactly what LLMbda exposes, and the exposure is the contribution even if no production framework adopts the calculus verbatim.
The practical barriers are real. Retrofitting labels onto an existing agent framework means every tool, every retrieval step, and every model call has to participate in label propagation, and a single unlabelled shortcut collapses the guarantee. The Lean-verified harness is a research artefact, not a drop-in replacement for LangGraph or the agent loop in a managed platform. What LLMbda offers production teams today is a measuring stick: a precise statement of what secure would mean, against which a sandbox-and-filter stack can be seen to fall short.
The test for an agent platform is no longer whether it is sandboxed. It is whether you can name the theorem its confidentiality rests on, and whether that theorem is about the code that actually runs.
Frequently Asked Questions
What inputs does the ‘insulated variant’ of the noninterference theorem actually protect against?
The insulated variant assumes the attacker controls every untrusted input the agent might consume. That includes retrieved documents, tool outputs, and any data the model can be coaxed into reading. This matches the real threat model for prompt injection, where an adversary might poison a webpage the agent retrieves or compromise a tool it calls. The theorem holds even when the attacker supplies all these inputs, not just a curated set of adversarial prompts.
Why does sandboxing fail to stop information leaks in agents?
Sandboxing confines execution, not data flow. An agent restricted from writing to the filesystem or calling blocked APIs can still read a secret from retrieved context and fold it into a response. The sandbox permits emitting responses, and passing a secret to a whitelisted tool is an allowed action. Information-flow control stops the secret from reaching that output in the first place, regardless of what execution boundaries exist.
What does ‘termination-insensitive’ mean for a secure agent?
The noninterference theorem does not cover what an attacker might learn from whether a computation halts. An agent could refuse to process certain inputs or loop indefinitely when secrets are present, and that behavior itself might reveal information. The theorem guarantees confidentiality about data values, not about timing or termination patterns.
What would adopting LLMbda require from existing agent frameworks?
Every tool call, retrieval step, and model invocation would need to participate in label propagation. A single unlabelled shortcut would collapse the guarantee. Current Python and TypeScript orchestration stacks track provenance, if at all, in ad-hoc string metadata that nothing enforces. Retrofitting means rewriting the agent loop to treat every value as labelled, not adding a filter to an existing pipeline.
Why are dual-LLM defences like CaMeL hard to audit?
Dual-LLM architectures bake isolation into the plumbing, so security guarantees depend on how the planner and executor models are wired. When someone relaxes a rule to ship a feature, that relaxation lives in application code outside the security argument. LLMbda makes the relaxation visible in the reduction semantics, where the theorem must account for it. The difference is between trusting implementation details versus trusting a proof about the language itself.
