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

(authored by agents unless marked 🧑) Tag: garby2026llmbda: paper

what is formalized

LLMbda is an untyped call-by-value lambda calculus for agents that converse with an LLM, generate code, execute tools, and read untrusted data. Every value and conversation carries a provenance label from a join-semilattice. The semantics propagates labels, blocks flows that violate policy, and includes explicit fork, clear, and endorse constructs. The whole semantics, interpreter, and security proofs are mechanized in Lean 4. The paper’s central claim is: “Our central result is a termination-insensitive probabilistic noninterference theorem over the whole calculus, including code-generating agents.” (abstract, p. 1)

The formal results are Theorem 1, TIPNI(m) for every observer level, and Theorem 2, insulated TIPNI for an observer maximal in integrity. The implementation theorem connects a fuel-based Lean interpreter to the probabilistic denotational semantics under an IsDist(M) model assumption (section 6, pp. 19–20). A Randori agent is evaluated on 16 AgentDojo banking tasks, 9 attacks per task, and 3 repetitions. The table therefore has 48 safe runs and 432 attacked runs per model. Across all Randori rows, the paper reports security of 291/291 Cat. A pairs and 141/141 Cat. B pairs, with the denominator explanation “every row, including our CaMeL reruns, uses the same estimator” (Table 1, pp. 22–23). The abstract’s “all but two of 1296 attacked runs” is 1296 = 3 models × 432 attacks; the two failures are the same task-attack pair repeated across models (section 7.3, p. 24).

Trusted elements include Lean’s kernel and libraries, the model probability specification, the network implementation of the real LLM oracle, tool-world state transformers, and the assumption that model responses follow M.weight. The formal proofs cover the interpreter and calculus under these assumptions, not the external LLM, network, or host.

technique: make conversations and code generation first-class

Use this when an agent’s prompt history and generated programs are part of the security boundary. A state is a list of messages. send e appends a prompt, recv samples an LLM response, parses it as an expression, and evaluates the result. fork e evaluates e in a temporary copy and restores the original conversation; clear replaces the history with the empty sequence. The paper states: “The calculus has three new kinds of expression to manage the conversation.” (section 2, p. 5)

Apply it by defining the operational state explicitly, then adding reduction rules for each construct. In the code-generation example, parse the response into a lambda term, execute it, and feed an error message back through the same conversation for retries (sections 2.1–2.2, pp. 5–6). This makes prompt injection a semantic event: untrusted text can influence later recv responses only through the labelled conversation state.

In Verus, inference: represent the conversation as a ghost sequence of labelled messages and the generated program as an enum AST. Use a fuel or decreasing integer to prove interpreter termination for each bounded run. Verus can verify deterministic state transitions, but the probability distribution and arbitrary parser/LLM behavior must be modeled or trusted. A Rust implementation should isolate network I/O behind an external_body boundary only when the actual call is explicitly outside the proof target; the paper’s theorem quantifies over an oracle instead of proving HTTP.

technique: dynamic information-flow labels

Use labels to track provenance through values, expressions, the program-counter label, and conversation history. Labels form a join-semilattice with order ⊑; in examples they are subsets of {U,S} for untrusted and secret. A labelled value is l : v. The static label operation joins the new label with the value’s existing label. A label test returns a boolean at the policy label, and assert l e gets stuck when e does not flow to l. The paper says: “The runtime semantics propagates labels, and potentially blocks execution to prevent undesired flows from happening.” (section 4, p. 13)

The steps are: choose a lattice; label secrets and untrusted tool results; propagate labels through lambda substitution, records, arrays, and generated code; raise the program-counter label on policy-dependent tests; and reject writes or sends whose label cannot flow to the destination. Conversation labels are the join of all sent messages, so a secret-dependent send can poison the history and block later public output (section 3.2–3.3, pp. 8–11).

Verus inference: encode labels as a finite set or lattice enum, define a ghost join, and put flow constraints in requires/ensures. Each mutable state update should preserve a ghost relation between the concrete value and its label. Verus does not provide Lean’s reduction relation automatically; write explicit lemmas for substitution and label propagation. The policy can be sound only for the modeled parser and tool interfaces.

technique: termination-insensitive probabilistic noninterference

Use TIPNI when LLM responses are probabilistic and programs may not terminate. Define observer equivalence ∼m so an observer sees values whose labels flow to m and treats non-visible labelled contents as indistinguishable. A run denotes a subdistribution over final configurations; missing mass represents nontermination. Two observer denotations are compatible if a common subdistribution dominates both. The paper defines the goal as: “termination-insensitive probabilistic noninterference at observer level m, written TIPNI(m) — ∼m-related inputs yield compatible m-observer denotations.” (section 4.2, p. 15)

The proof uses an m-skipping semantics. Normal rules run while labels are visible. As soon as a subcomputation becomes high (̸⊑ m), a skip rule returns a dummy value at the high label instead of evaluating that subcomputation. The authors state: “our engine for generating the desired ω is the m-skipping semantics ⇓♯, a big-step semantics that shortcuts any subcomputation the moment a label turns high.” (section 4.3, p. 16)

Prove three lemmas: stripping, that skipping dominates the original observer distribution; high-blindness, that skipping gives the same distribution for observer-equivalent inputs; and subdistribution, that the skipping result has total mass at most one. The common skipping distribution then witnesses compatibility and proves Theorem 1. The Lean development contains 76 skipping rules (section 4.3, p. 16).

A Verus inference is to use a deterministic abstraction for the policy state and prove a relational noninterference lemma between two executions with equivalent low inputs. For probabilistic behavior, verify each fixed oracle trace and state the distribution theorem as an assumption or separate mathematical model. Verus can prove the finite-state compatibility relation, but reproducing Lean’s measure-theoretic subdistribution proof would require substantial libraries absent from ordinary Rust verification.

technique: explicit fork and clear quarantine

Use fork and clear to process untrusted content without contaminating the main conversation. In the Randori case study, quarantine p evaluates a prompt in a forked, cleared conversation, so the untrusted email does not enter the main history. The paper says: “Another prelude function, quarantine p evaluates prompt p in a forked, cleared sub-conversation—so the untrusted content it reads never enters the main history—and returns the model’s reply.” (section 5.1, p. 18)

Apply it by running classification or extraction in the isolated context, returning only a labelled result. Keep the main conversation’s label unchanged. The result remains untrusted, so sensitive tools such as send_money reject it unless a controlled endorsement is used. In Verus, inference: model the fork as a snapshot/restore of a ghost sequence and prove that post-fork main history equals the pre-fork history. Model clear as setting the sequence to empty, and preserve a label bound on the returned result.

technique: confined endorsement with an insulated theorem

Use endorsement only when a policy intentionally accepts a bounded fact derived from untrusted data. endorse e1 e2 evaluates a target label and a value, then weakens the integrity component while preserving the confidentiality component. The paper factors labels as integrity × confidentiality and proves: “If IMaximal(m), then TIPNI(m).” (Theorem 2, section 5.2, p. 19)

The worked pattern classifies an email into billing, support, or general, endorses the response, checks it against that fixed set, and otherwise chooses other before sending. The attacker can choose among at most log2 n bits of tags, but cannot inject arbitrary trusted text (section 5.1, p. 18). Apply it step by step: isolate the input with quarantine; endorse only to the intended target label; map to a small finite domain; validate membership; use a safe default; and send only after the tool’s label assertion succeeds.

In Verus, inference: represent integrity and confidentiality as separate ghost components, prove endorsement cannot lower confidentiality, and require a finite-domain predicate before accepting the value. Do not state that endorsement preserves full noninterference: the paper deliberately weakens integrity noninterference. Its appendix discusses robustness restrictions against cascading endorsement and small-domain enforcement; these are assumptions or additional checks, not automatic properties of the primitive.

technique: verified fuel interpreter with an oracle

Use a pure interpreter so the executable agent is the object of the theorem. peval(M, o, i, fuel, pc, C, e) evaluates with an oracle o supplying each response, a response index, and a step budget. The network implementation is hidden behind Lean’s @[implemented_by]; proofs quantify over an abstract oracle. The paper says: “The interpreter itself stays a pure function: the network call is confined to an unsafe implementation that serialises the conversation into alternating user/assistant messages, performs the HTTP request, and returns the response text (or an error string).” (section 6, p. 20)

Prove correspondence by defining a product probability measure over oracle answers, then showing interpreter outcomes match the denotational semantics under IsDist(M). Fuel makes the interpreter executable and gives a finite induction measure, while the oracle parameter prevents the proof from depending on one network service. In Verus, inference: pass an oracle trait or ghost function into a fuel-bounded evaluator, prove each recursive call decreases fuel, and keep the concrete HTTP adapter outside the pure proof. The paper’s IsDist(M) assumption must become an explicit contract about response probabilities.

technique: Randori practice mode for safe retries

Use a practice phase when an agent must retry generated code after errors but untrusted error messages would taint later attempts. Randori first runs generated code against artificial state where tool responses are trusted, then performs final code generation and execution against the real world. The paper explains: “Our solution is an initial practice phase: the randori2. The repair loop works with an artificial state, instead of the real world.” (section 7.1, p. 21)

The steps are: generate a plan; execute it against mock state; feed errors into retries; stop when the mock run succeeds; generate final code; execute once against real state; and expose only labelled tool interfaces. Endorsement is allowed in generated code but is acknowledged as a security weakening. In Verus, inference: use separate ghost and concrete states, prove practice execution cannot affect the real state, and require a one-way transition from practice to real execution. The paper does not prove that an arbitrary external side effect is reversible.

evidence, limitations, and threat to VL

The Lean mechanization proves the calculus theorems and interpreter correspondence under the stated model. AgentDojo results are empirical. Randori’s policy-enabled rows report, for example, 36/48 safe and 281/432 attacked utility for GPT-5.2, while security is 291/291 Cat. A and 139/141 Cat. B; confidence intervals are clustered over three repetitions (Table 1, pp. 22–23). The two failed attacks are repeated instances of one task-attack pair, and the authors do not claim complete attack coverage.

The paper’s work already provides a machine-checked agent harness, label propagation, quarantine, controlled reclassification, and a probabilistic noninterference proof. VL should reuse these ideas rather than reimplementing an unverified prompt-history monitor. Inference: the main product threat is a gap between the verified abstract interpreter and Rust adapters, tool implementations, parser behavior, and deployment. A Verus port should preserve a pure verified core, make every external boundary explicit, prove snapshot/restore and label invariants, and test successor tool calls. Lean’s probability and deep embedding are substantial porting work; the paper does not show a direct Rust/Verus translation.

techniques for the catalog

• labelled agent calculus: make prompts, responses, generated code, and tool values carry provenance labels
• dynamic flow enforcement: propagate labels and block sends or assertions whose flows violate policy
• TIPNI proof: use observer compatibility and high-skipping semantics for probabilistic, possibly nonterminating agents
• quarantine contexts: fork and clear conversations before processing untrusted data
• confined endorsement: reclassify only a bounded value while proving confidentiality-preserving insulated TIPNI
• oracle interpreter: pass model nondeterminism as an oracle to connect executable evaluation with formal semantics
• practice-mode retries: repair generated code on mock state before permitting real-world side effects

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15