# The LLMbda Calculus: AI Agents, Conversations, and Information Flow

arXiv: https://arxiv.org/abs/2602.20064 · HTML: https://mlsanity.com/paper/2602.20064/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in Agent threats, guardrails and governance, one of 16 directions in LLM agents and tool use.
- Builds on 20 of its 58 references that are in the map.
- First posted on arXiv 23 Feb 2026.

## Placed in

- LLM agents and tool use / [Agent threats, guardrails and governance](https://mlsanity.com/agents/agent-threats-guardrails-and-governance/)

## Builds on (most cited first, 20 of 20)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [Sequence to Sequence Learning with Neural Networks](https://mlsanity.com/paper/1409.3215/) (2014)
- [SWE-agent: Agent-Computer Interfaces Enable Automated Software Engineering](https://mlsanity.com/paper/2405.15793/) (2024)
- [Not what you've signed up for: Compromising Real-World LLM-Integrated Applications with Indirect Prompt Injection](https://mlsanity.com/paper/2302.12173/) (2023)
- [Formalizing and Benchmarking Prompt Injection Attacks and Defenses](https://mlsanity.com/paper/2310.12815/) (2023)
- [Defeating Prompt Injections by Design](https://mlsanity.com/paper/2503.18813/) (2025)
- [Defending Against Indirect Prompt Injection Attacks With Spotlighting](https://mlsanity.com/paper/2403.14720/) (2024)
- [Securing AI Agents with Information-Flow Control](https://mlsanity.com/paper/2505.23643/) (2025)
- [The Task Shield: Enforcing Task Alignment to Defend Against Indirect Prompt Injection in LLM Agents](https://mlsanity.com/paper/2412.16682/) (2024)
- [System-Level Defense against Indirect Prompt Injection Attacks: An Information Flow Control Perspective](https://mlsanity.com/paper/2409.19091/) (2024)
- [Prompt Flow Integrity to Prevent Privilege Escalation in LLM Agents](https://mlsanity.com/paper/2503.15547/) (2025)
- [ACE: A Security Architecture for LLM-Integrated App Systems](https://mlsanity.com/paper/2504.20984/) (2025)
- [A Lambda-Calculus Foundation for Universal Probabilistic Programming](https://mlsanity.com/paper/1512.08990/) (2015)
- [Opportunistically Parallel Lambda Calculus](https://mlsanity.com/paper/2405.11361/) (2024)
- [Quasar: A Programming Language Specialized for LLM Code Actions](https://mlsanity.com/paper/2506.12202/) (2025)
- [On Dynamic Flow-Sensitive Floating-Label Systems](https://mlsanity.com/paper/1507.06189/) (2015)
- [Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis](https://mlsanity.com/paper/1506.03950/) (2015)

## Built on by (most cited first, 4 of 4)

- [Formal Analysis and Supply Chain Security for Agentic AI Skills](https://mlsanity.com/paper/2603.00195/) (2026)
- [The Y-Combinator for LLMs: Solving Long-Context Rot with λ-Calculus](https://mlsanity.com/paper/2603.20105/) (2026)
- [Formal Semantics for Agentic Tool Protocols: A Process Calculus Approach](https://mlsanity.com/paper/2603.24747/) (2026)
- [L3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agents](https://mlsanity.com/paper/2610.19591/) (2026)

## Abstract (arXiv)

Large language models are increasingly deployed as agents: they plan, call tools, read untrusted data, and act on the results. This exposes them to prompt injection: data meant only to be read is obeyed as an instruction. The most principled defences replace content inspection with provenance: classifying data by source and keeping trusted and untrusted apart through a separation of duty (the dual-LLM pattern) and information-flow control. Yet the leading systems are hard to fully trust: flow tracking is easy to get wrong, deliberate relaxations are hard to audit, and the dual-LLM pattern is hard-wired into the architecture. We present LLMbda, an untyped call-by-value lambda calculus that makes provenance-based defence both expressible and provably sound, without committing to an architecture. It adds the operational core of agentic systems as first-class constructs: prompt-response conversations that can be forked and cleared, code generation, and dynamic information-flow control in which every value carries a label that every reduction propagates. Isolation becomes a policy a program expresses, and reclassification an explicit, auditable construct. Our central result is a termination-insensitive probabilistic noninterference theorem over the whole calculus, including code-generating agents, with an insulated variant that holds even when the attacker chooses all untrusted inputs. The verified interpreter is itself the harness that calls the model, to our knowledge the first LLM agent harness whose executable is the subject of machine-checked security theorems, so every agent inherits the guarantee. On the AgentDojo banking benchmark, an agent built within LLMbda, enforcement always on, matches the utility of CaMeL, a leading dual-LLM defence, run without its policy checks (which halve its utility), and resists all but two of 1296 attacked runs. Our harness and all proofs are in Lean.