The LLMbda calculus: AI agents, dialogue and information flow

Core question: how to provide LLM agents with a prompt injection defense that is both expressive and provably sound, without baking a fixed architecture (such as dual-LLM) into the framework.

• Scenario and importance: LLM agents plan, call tools, read untrusted data, and act on it, which the authors state exposes them to prompt injection—data that should only be read is executed as instructions. Defenses based on content inspection (classifiers, asking the model whether the input looks like an attack) are an arms race, which the authors believe guarantees nothing.
• Shortcomings of existing methods: the authors point out that the provenance approach (dual-LLM separation of duties + IFC) has three difficulties: IFC is error-prone at boundaries (the text gives two leakage examples for CaMeL: a classic leak where labels of untaken branches are not updated, and an untracked Python retry loop that iterates a termination bit into a full secret); deliberately relaxed tracking (e.g., FIDES not tracking data-dependent control flow, leaving a small-domain value escape hatch) is hard to audit; and both CaMeL and FIDES hard-code the dual-LLM split into the architecture, and CaMeL has no comparable soundness theorem.
• Core observation: the authors believe the isolation guarantee of dual-LLM can be subsumed by the IFC guarantee—as long as session mechanisms such as forking, clearing, and prompting become programmable primitives, isolation becomes a policy expressed by the program rather than a shape imposed by the framework.
• What the paper proposes: the LLMbda calculus (sessions, code generation, and dynamic IFC as first-class constructs), TIPNI and Insulated TIPNI theorems for the full calculus (mechanized in Lean 4), an executable interpreter covered by machine-checked theorems, and the Randori agent evaluated on AgentDojo banking.
• Threat model:
  • Attacker goal: inject instructions through untrusted data to make the agent perform unintended actions (e.g., send emails, transfer money).
  • Attacker knowledge/capability: controls untrusted inputs; Insulated TIPNI holds even when the attacker chooses all untrusted inputs (per the authors).
  • Victim system: an LLM agent that calls tools and maintains prompt-response sessions.
  • Defender assumptions: data is labeled by provenance (trusted/untrusted, secret), and tool library developers place label checks at sensitive sinks.

Information-flow-based injection defenses

• CaMeL [20]—a refinement of dual-LLM, in which a privileged model generates and runs code; the paper criticizes two leaks in its IFC sublanguage (§1), and there is no comparable soundness theorem; the CaMeL authors themselves call formalization a "crucial direction."
• FIDES [18]—combines separation of duties with IFC; the paper points out that it deliberately does not track data-dependent control flow and provides a small-domain escape hatch, and that its confidentiality guarantee is taint-tracking (explicit secrecy [58]).
• Wu et al. [75], Kim et al. [37], Li et al. [42]—respectively prove noninterference for a fixed system architecture, dynamically track untrusted sources, and statically analyze an output planning language.

Foundations of linguistic IFC

• Austin and Flanagan [7, 8]—purely dynamic information flow and the labelled lambda calculus; the labeling mechanism in this paper is closest to this; the paper points out that the label test in [7] proves noninterference only for a two-point lattice, and that its test semantics applies only to a two-point lattice.
• Bichhawat et al. [10]—achieves an arbitrary lattice but omits the test; LIO [15, 63, 66]—labels are first-class values; Zheng and Myers [79], Tse and Zdancewic [64]—labels/principals computed at runtime.
• Hunt, Sands and Stucki [34]—a general recipe for weakening domain-theoretic information-flow properties to termination-insensitive versions; this paper defines TIPNI accordingly; Smith and Alpízar [61] and Unruh [65] proposed properties equivalent to TIPNI.

Calculi and probabilistic programming for LLMs

• OPAL [46], Quasar [47]—lambda-calculus languages for LLMs; the paper points out that neither handles prompt injection or noninterference.
• Zar [9], Borgström et al. [13], Kozen [39], Wand et al. [68]—verified samplers and semantic correspondences for probabilistic programs; Theorem 3 is of the same kind but stated directly as a measure equality.

LLM tools in Lean and other defenses

• Lean Copilot [62], LLMstep [70], LeanAide [25]—invoke LLMs to assist proof development and prove no property of the harness; Lean4Agent [69] verifies Hoare-style pre- and postconditions of workflows, but the agent runs outside Lean.
• LBAC/TypeGuard [80] (Haskell type-checked capabilities) and tacit [50] (Scala 3 capture checking)—contemporaneous typed harnesses; the paper compares evaluation results with them in §7.3. Spotlighting [33], Task Shield [35]—non-IFC injection defenses.

Baselines and benchmark: the comparison baseline is CaMeL (rerun by the authors, in two settings with policy on/off), and the benchmark is the banking suite of AgentDojo [21].

Authors' positioning: LLMbda is what the authors call the first LLM agent harness whose executable file is itself the object of a machine-checked safety theorem; its guarantee is a metatheorem covering the entire calculus (including code-generating agents), rather than being tied to a fixed planner shape.

Overall approach: make the operational core of the agent system a first-class construct of an untyped call-by-value lambda calculus LLMbda, where every value carries a label and every reduction rule propagates labels; isolation becomes a policy expressed by the program, reclassification (endorse) becomes an explicit auditable construct; all semantics and theorems are mechanized in Lean 4.

Sessions and code generation

• State is a session (message list) with the LLM; send e appends the serialized prompt to the session, recv samples a response from the model according to the current session and parses it into an expression to continue evaluation; the derived form @e ≜ (λ_. recv) (send e).
• fork e evaluates on a temporary copy of the session and then discards it, clear clears the session; the two make dual-LLM-style isolation a programmable policy (e.g., the prelude function quarantine processes untrusted content in a fork+clear sub-session).
• Code generation: responses can be parsed as lambda abstractions and executed; §2 gives an example generation loop with syntax hints and retries.

Labels and dynamic IFC

• Labels are taken from a join-semilattice (⊔, ⊑, ⊤, ⊥), the example uses the four-point lattice of the power set of {U, S}; values are labeled ⊥ by default (parsimonious principle), and the session state label is the upper bound of all sent messages.
• Primitives: static/dynamic label expressions l:e and e1:e2, test e1?e2, assertion assert e1 e2 (evaluation gets stuck on violation, the interpreter reports a runtime error).
• Label tests return the result to pc⊔l (the label of the tested policy) rather than the data's own label, which the authors say makes tests noninterferent; in contrast [7] returns to bare pc and is sound only for the two-point lattice.
• Probabilistic big-step semantics pc \vdash C, e \Downarrow C', V \triangleright w, s: consumes the sampling trace s, joint probability w; Confinement (Lemma 1) guarantees pc is not higher than the result label.

TIPNI and proof technique

• Indistinguishability ∼n: identical for an observer that can only see labels ⊑ n; the denotation of a configuration is a sub-distribution over final states, and the missing mass is the nontermination probability.
• TIPNI definition: \mathrm{TIPNI}(m) \triangleq C_0 \sim_m C_1 \land e_0 \sim_m e_1 \Rightarrow \llbracket pc \vdash C_0, e_0 \rrbracket_m \smile \llbracket pc \vdash C_1, e_1 \rrbracket_m, i.e., ∼m-related inputs produce compatible (there exists a common dominating sub-distribution) m-observer denotations; derived from the general recipe of [34].
• Properties: coincides with TINI in the deterministic case (Lemma 3), coincides with PNI under total termination (Lemma 4), leakage is bounded by the average nontermination probability (Lemma 5); the authors note it is equivalent to existing properties in [61], [65].
• Proof technique (which the authors call a contribution): define an m-skipping semantics ⇓♯ that short-circuits to a dummy value {} when the label becomes high (̸⊑ m); construct the witness ω via three mechanized lemmas: stripping (dominates the original semantics), high-blindness (returns the same distribution on ∼m inputs), and sub-distribution. The full rule set of 76 rules is in the Lean development.

Endorse and Insulated TIPNI

• endorse e1 e2 reclassifies the integrity axis of e2 to the label specified by e1; the lattice factors into two dimensions, integrity × confidentiality (L ≅ I × S), and weakening is limited to the chosen dimension.
• Insulated TIPNI (Theorem 2): TIPNI holds for I-maximal observers (ignoring the integrity axis)—the authors say this means that even if the attacker chooses all untrusted inputs and endorses arbitrary reclassifications, the confidentiality guarantee is unaffected.
• Appendix E gives two constrained variants that do not change the semantics: robust_endorse (endorsed bits block cascading) and bounded_endorse (small domain, at most log2 n bits); the authors leave formal quantitative bounds as future work.

Implementation and evaluation method

• The interpreter peval is a pure function in Lean that threads fuel, with an oracle supplying the response for each recv; in real runs the oracle sends HTTP requests via an unsafe implementation, but for the proofs it is just some universally quantified oracle.
• Theorem 3 (oracular correctness): the distribution obtained by first sampling the oracle and then running the deterministic interpreter equals the denotational semantics of §3 (assuming responses are distributed according to M.weight and total mass is 1).
• Randori agent: dual-LLM architecture, the P-LLM generates code, the Q-LLM isolates and processes untrusted data; the randori practice phase first runs a repair loop on mock state (tool responses are always trusted), then generates the final code to execute in the real world; the code generation phase is allowed to endorse specific data flows in advance.

Experimental Setup

• Models under test: three—GPT-5.2, Qwen3.7-plus, MiMo-v2.5—with the same model serving both the code generation (P-LLM) and isolated Q-LLM roles.
• Benchmark: the AgentDojo banking suite, 16 user tasks × 9 injection attacks = 144 task/attack pairs, each pair repeated k = 3 times.
• Baseline: the authors' rerun of CaMeL, in two rows, (no policy) (policy checks off) and (with policy) (policy checks on), run only on the two models GPT-5.2 and MiMo-v2.5.
• Metrics: Utility (proportion of user tasks correctly completed, in Safe/Attacked columns, 95% Student-t confidence intervals, with tasks or task/attack pairs as the sampling unit); Security (number of pairs where the attack was successfully repelled, stratified by Category A/B, 95% Wilson score intervals).
• Category division: Category A (97/144) is the case where the tool calls required by the attack would not appear in the generated code anyway; Category B (47/144) is the remaining cases where the generated plan suffices for the attack to succeed.
• Ablation: Randori (no endorse) removes the endorse capability; IFC enforcement is always on in all Randori rows.

Main Results

According to Table 1 (AgentDojo banking, 16 tasks × 9 attacks, k = 3):

Swipe horizontally to read the table

System	Model	Utility Safe	Utility Attacked	Security Cat. A	Security Cat. B
Randori	GPT-5.2	36/48 (75% ± 18.9)	281/432 (65% ± 6.7)	291/291 [96.2, 100]	139/141 [90, 99.8]
Randori	Qwen3.7-plus	36/48 (75% ± 20.0)	274/432 (63.4% ± 6.8)	291/291 [96.2, 100]	141/141 [92.4, 100]
Randori	MiMo-v2.5	31/48 (64.6% ± 22.0)	257/432 (59.5% ± 6.2)	291/291 [96.2, 100]	141/141 [92.4, 100]
Randori (no endorse)	Qwen3.7-plus	30/48 (62.5% ± 24.2)	260/432 (60.2% ± 7.2)	291/291 [96.2, 100]	141/141 [92.4, 100]
Randori (no endorse)	MiMo-v2.5	26/48 (54.2% ± 23.3)	243/432 (56.2% ± 6.8)	291/291 [96.2, 100]	141/141 [92.4, 100]
CaMeL (no policy)	GPT-5.2	32/48 (66.7% ± 23.4)	96/135 (71.1% ± 7.7)	98/99 [94.4, 99.8]	141/141 [92.4, 100]
CaMeL (no policy)	MiMo-v2.5	34/48 (70.8% ± 21.4)	104/144 (72.2% ± 7.4)	240/241 [95.3, 99.9]	138/141 [88.9, 99.6]
CaMeL (with policy)	GPT-5.2	18/48 (37.5% ± 26.6)	70/233 (30% ± 8.1)	97/97 [96.1, 100]	134/134 [92.4, 100]

• The authors state: Randori (policy always on) has utility comparable to CaMeL (no policy) within confidence intervals, about twice that of CaMeL (with policy) (37.5%); the table note states that some CaMeL attacked/security runs were not completed, and its cells count only completed runs.
• The authors state that Randori was broken in only 2 of 1296 attacked runs (both Category B runs of the same task/attack pair under GPT-5.2); the authors consider this attack semantic and beyond the scope of IFC defense, and that it would be blocked without endorse.
• The authors point out that CaMeL (no policy) has 2 Category A failures on GPT-5.2: in task 12 the agent implemented an "interpreter loop" that, without policy checks, lets the attacker bypass the dual-LLM pattern.

Security-Utility Tradeoff Comparison with Contemporaneous Systems

• The authors cite TypeGuard (a Haskell implementation of LBAC) results on the AgentDojo slack suite: with policy enabled, utility drops from 15/21 to 8/21 (38.1%), and under the same conditions CaMeL is 7/21; the authors state this matches CaMeL's utility-decline pattern.
• The authors cite contemporaneous reports: TypeGuard repels all 105 slack injection pairs, and tacit fails only once in 2 × 963 trials across four stock suites and two models; a paper footnote notes that cross-paper numbers are for reference only (suites, models, attack sets, and repetition counts all differ).
• The authors believe their Category A/B decomposition shows that about two-thirds of banking pairs can be repelled by a "plan first, then expose" architecture alone, and point out that TypeGuard and tacit deliberately give up code/data separation, so every task-attack pair effectively falls into Category B.

Failure Cases and Ablation Interpretation

• Two successful attacks: the task requires reading a file and paying according to its content, and the injection replaces the file content with a malicious payment request; the authors state this is a semantic attack, and the only way to block it at the IFC level is to indiscriminately prevent any untrusted file content from being "laundered."
• (no endorse) ablation: utility drops (see table), which the authors state confirms endorse is necessary for some tasks—tasks 0, 2, and 12 require reading untrusted files and performing actions whose trust is asserted; the authors also state that restoring endorse buys back these tasks at the controllable cost of Category B security.
• Randori's disadvantages: the authors point out that LLMbda syntax is entirely new and not in training data, and that it lacks native error handling, so many runtime errors cannot be caught by the monadic safe version, and information-flow errors are not thrown during the randori phase.

Other Ablations and Analyses

• Of the two successful injections in the CaMeL paper itself, one is the same document-directed payment case (CaMeL placed outside the threat model), and the other is in the travel suite, where a verbatim quote of a hotel review triggers AgentDojo's string-matching criterion; the authors state that four independent systems converge on the same residual case, supporting reading it as the semantic limit of IFC defenses.
• The authors state that while studying the CaMeL interpreter they found unexpected taint propagation rules (e.g., interpolating an untrusted value into a string literal implicitly makes it trusted), and believe their noninterference theorem rules out such flaws in the LLMbda interpreter.
• Appendix E.5 uses six small examples that do not call an LLM to probe endorse semantics (laundering {U}→{}, not lowering confidentiality, inertness under a tainted pc, value pass-through, error on illegal targets, and lifting the test for subsequent flows).

Limitations and future directions noted by the authors

• Data source modeling (§9 Conclusion): the modeling of tool calls and data sources assumes all data sources are within the program; the authors believe a better model should allow LLMbda functional programs to interact generally with external data and tools.
• Risk of endorse misuse (§9): plans containing endorse can launder untrusted data past the checks—the two successful attacks in §7.3 are exactly this—and there is no mechanism to stop an overly permissive planner from endorsing at will; the authors say distilling constraint rules into design guidelines (e.g., static analysis of plans before execution) is future work.
• Benchmark extension (start of §7): the authors plan to benchmark in the future on the full AgentDojo suite with the full CaMeL policy; currently only a subset of the CaMeL policy is implemented and only the banking subset is run.
• Error handling (§D.4): the authors say a major weakness of Randori is that LLMbda lacks error recovery, and future work could consider error handling as a language primitive or moving to a total language without runtime errors, and exposing information flow errors during the randori phase.
• Type system and syntax (§D.4): the authors believe a minimal type checker could statically reject problematic plans; for the utility cost caused by syntax not being in the training data, the authors suggest syntax-constrained decoding or surface syntax closer to mainstream languages.
• Robust/quantitative endorse (§E.2, §E.3): developing the knowledge-based definition in the probabilistic setting is left as future work; formal quantitative bounds for bounded_endorse are also left as future work.

Experimental coverage

• The models tested are GPT-5.2, Qwen3.7-plus, MiMo-v2.5, 3 in total; the CaMeL rerun covers only two of them, GPT-5.2 and MiMo-v2.5 (Table 1).
• The benchmark is only the AgentDojo banking suite: 16 user tasks × 9 injection attacks, k = 3 repetitions; some CaMeL attacked/safe runs were not completed, and its cells count only completed runs (Table 1 note).
• The ablation is only (no endorse), and is reported only on the two models Qwen3.7-plus and MiMo-v2.5 (Table 1).
• The paper does not report a judge model or LLM judge: utility and security are determined by AgentDojo's task/security checkers (§D.2), and the paper does not state their specific judging model.
• The same model serves as both code generator and Q-LLM; the paper does not evaluate the setting of replacing the Q-LLM with a smaller model, and §D.4 says the interpreter currently does not support multiple models.

A formal methods + systems paper: the authors propose the LLMbda calculus for defending LLM agents against prompt injection, and complete all mechanized proofs and an executable interpreter in Lean 4.

• Problem: the authors believe the IFC of existing provenance defenses (CaMeL, FIDES) is error-prone at the boundaries, deliberate relaxations are hard to audit, and dual-LLM architectures are hard-wired and lack soundness theorems covering code-generating agents.
• Method: LLMbda makes prompt-response sessions (@, fork, clear), code generation and dynamic IFC first-class constructs, with every value carrying a label and every reduction propagating labels; endorse is an explicit auditable reclassification. The authors prove TIPNI for the full calculus (Theorem 1) and Insulated TIPNI (Theorem 2, confidentiality still holds when the attacker chooses all untrusted inputs), as well as oracular correctness of the interpreter (Theorem 3); the authors say it is the first LLM agent harness whose executable file is itself a machine-checked theorem object.
• Result 1: on AgentDojo banking (16 tasks × 9 attacks, k = 3), Randori (IFC always on) has attacked utility of 59.5%–65% (three models), comparable within confidence intervals to CaMeL (no policy); CaMeL (with policy) safe utility drops to 37.5% (Table 1).
• Result 2: Randori was compromised only 2 times out of 1296 attacked runs, both being the same semantic attack under GPT-5.2 (read a file and pay according to its content); the authors believe this is beyond the scope of IFC defenses.
• Result 3: the (no endorse) ablation shows a utility drop (e.g., MiMo-v2.5 safe from 64.6% to 54.2%), which the authors say confirms that endorse is necessary for tasks that read untrusted files and perform trusted actions.
• Conclusion and implications: the authors believe isolation should be a policy expressed by the program rather than a shape imposed by the framework; the authors also acknowledge that plans containing endorse can bypass the checks, and list design guidelines constraining endorse and full-suite benchmarking as future work.