{"id":"4ea5d236-3eb5-4981-a7e4-2ed617e0a933","arxiv_id":"2602.20064","paper_version":2,"verdict":"REJECT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A call-by-value lambda calculus with LLM generation and dynamic labels is shown to satisfy termination-insensitive noninterference on a restricted fragment, with a supposedly Lean-verified interpreter.","lead":"A new lambda calculus for AI agents adds LLM calls, conversation forks and clears, and data labels, and proves a termination-insensitive noninterference theorem for a restricted fragment. If sound, it gives a generic formal foundation for provenance-based prompt-injection defenses instead of fixed architectures.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Abstract overclaims: whole-calculus probabilistic TINI and Lean-verified proofs are not what the body proves; Theorem 1 is restricted and its appendix proof is only a sketch.","rationale":"The reader's verdict is REJECT, and I agree the paper in its current form should not be accepted. The reader's weakest assumption focuses on the serialisation step in the PROMPT case; my analysis shows that step may be derivable from Lemma 2 plus functionality of serialise, so the bigger load-bearing issue is that the abstract promises a stronger and mechanised result than the body delivers. The body itself disproves the abstract's whole-calculus TINI claim, and the appendix proof is only a sketch with an unproved key lemma. The missing Lean artifacts are decisive evidence that the central claim is unverified. My concern is therefore broader than the reader's: even if the serialisation step is repaired, the paper still would not support its headline statement. Thus I recommend the same verdict (REJECT) and mark agreement as partial because I am not singling out the serialisation assumption as the core defect.","tokens_in":26928,"tokens_out":14801,"duration_ms":126467,"concrete_test":"Run the Section IV counterexample (M?(M:true) vs M?(M:H:false)) through the paper's own semantics (or the claimed interpreter) and verify that the two M-indistinguishable expressions produce distinguishable results, directly refuting any whole-calculus TINI claim. Additionally, obtain the Lean development referenced in the abstract and check whether Lemma 2 and the (PROMPT) case are proved there; if no Lean files are provided, the 'all proofs are in Lean' claim is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim, as advertised in the abstract, is a 'termination-insensitive probabilistic noninterference theorem over the whole calculus' with 'all proofs in Lean.' The body instead proves a deterministic TINI (Definition 1, Theorem 1) restricted to three sublanguages: expressions without ?, expressions using only one non-bottom label, and expressions where ? appears only via assert or strong test. Section IV explicitly gives a counterexample (M:true vs M:(H:false)) showing the full calculus does not satisfy TINI. Thus the abstract's unrestricted claim is false for the submitted semantics. Moreover, the appendix proof of Theorem 1 is not a complete formal proof: Lemma 2 (the erasure property 'v∼_n v′ implies erase_n(v)=erase_n(v′)') is stated without proof, and the (PROMPT) case invokes an unstated 'serialisation assumption' to conclude that v_0∼_k v_1 implies p_0=p_1. The promised Lean artifacts are absent from the submission, so the machine-checked verification claim is unsupported. These gaps mean the headline guarantee is not established; the paper cannot be accepted as is.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces LLMbda, an untyped call-by-value lambda calculus with dynamic information-flow control and primitives for LLM conversation management (@, fork, clear). It provides a big-step operational semantics with label propagation, a deterministic abstraction of LLM generation via serialise/parse/generate functions, and states a termination-insensitive noninterference (TINI) theorem restricted to three sublanguages: expressions without label tests, expressions using only one non-bottom label, and expressions where tests occur only via assert or strong tests. The paper also describes a Python interpreter and illustrates the calculus on postcode extraction, repair loops, a tool-calling agent, and a CaMeL-style code-generation defence. The abstract, however, claims a probabilistic noninterference theorem over the whole calculus, a machine-checked Lean proof, and a specific AgentDojo benchmark result, none of which is supported by the body of the paper.","tokens_in":27243,"tokens_out":4353,"duration_ms":44003,"significance":"The core idea of modelling LLM-agent conversations as first-class constructs in a lambda calculus with information-flow labels is timely and potentially valuable. The big-step semantics is written with care, and the explicit identification of a counterexample showing that unrestricted label testing breaks TINI is an honest and useful contribution. The restricted TINI statements, if fully proved, would be a meaningful formal foundation for provenance-based prompt-injection defences. However, the paper's headline claims — whole-calculus probabilistic noninterference, Lean-verified proofs, and a concrete AgentDojo result — are not established by the submitted manuscript. The appendix proof of the main theorem contains load-bearing gaps, and no machine-checked artifacts are provided. The significance of the work as presented is therefore substantially lower than advertised.","major_comments":[{"comment":"The abstract states a 'termination-insensitive probabilistic noninterference theorem over the whole calculus' and claims all proofs are in Lean. The body proves only a deterministic TINI for three restricted sublanguages (Theorem 1). Section IV explicitly presents a counterexample (M:true vs M:(H:false)) showing the full calculus does not satisfy TINI, and Section III-D assumes a deterministic generation function J·K; Section I.H lists probabilistic semantics as future work. The abstract's unrestricted probabilistic claim is therefore false for the submitted semantics, and the Lean-verification claim is unsupported because no Lean artifacts appear anywhere in the manuscript.","section":"Abstract; Section IV; Section III-D; Section I.H"},{"comment":"The proof of Theorem 1 is incomplete in a load-bearing way. In the PROMPT case, the argument requires that if n_i ⊑ k and v_0 ∼_k v_1 then serialise(erase_{n_i}(v_0)) = serialise(erase_{n_i}(v_1)); the text invokes an unstated 'serialisation assumption'. This property is not included in the semantics, in Definition 1, or in the statement of Theorem 1. If serialise formats labelled subterms differently, the conclusion fails. Lemma 2, the central erasure property that v ∼_n v' implies erase_n(v)=erase_n(v'), is also stated without proof and is needed for the erasure-based reasoning. These omissions mean the main theorem is not actually proved as written; the gaps could be repaired by adding explicit axioms and completing the induction, but they are not merely cosmetic.","section":"Appendix A, PROMPT case; Lemma 2"},{"comment":"The abstract claims 'Our harness and all proofs are in Lean' and describes 'the first LLM agent harness whose executable is the subject of machine-checked security theorems'. The implementation described in Section V is a Python interpreter (approximately 4000 lines) using the OpenAI Responses API, with no mention of Lean, no proof scripts, and no repository link. The machine-checked verification claim is thus unsupported by the submission. If the Lean formalisation exists, it needs to be provided or at least cited with a clear artifact identifier; without it, the central advertised contribution cannot be assessed.","section":"Abstract; Section V"},{"comment":"The abstract reports a specific empirical result: 'an agent built within LLMbda, enforcement always on, matches the utility of CaMeL ... and resists all but two of 1296 attacked runs'. The body contains no benchmark section, no experimental setup, no baseline definition, no hyperparameter details, and no presentation of these 1296 runs. This empirical claim is therefore unverifiable from the manuscript as submitted and should either be removed or supported by a proper evaluation section.","section":"Abstract (AgentDojo claim)"}],"minor_comments":[{"comment":"The ASSERT case of the proof is sketched more briefly than the rest. In particular, the treatment of the divergent else-branch Ω and the role of termination-insensitivity should be made explicit. As written, 'since both computations return the same labelled value' glosses over the case analysis needed when one side of the assert diverges.","section":"Appendix A, ASSERT case"},{"comment":"Lemma 3 says the derived rules for assert and strong test are 'sound and complete'. Completeness is not defined in the paper; it would be helpful to state the intended notion (e.g., derivability equivalence with the encoding) to avoid confusion.","section":"Section IV, Lemma 3"},{"comment":"There is a typographical inconsistency: 'Willitson' appears where 'Willison' is intended (the same author is correctly spelled elsewhere, e.g., references [8], [11]).","section":"Section VI.B"},{"comment":"The definition of erase_n is given by equations but the paper does not specify an ordering or pattern-matching convention for the rules; for example, the second equation could overlap with the first if fork expressions could be labelled. It would be clearer to state that erasure is defined by recursion on the expression structure and that labels intercept at the top level.","section":"Section III-D"},{"comment":"The paper would benefit from a short table of the labels used in the proof (pc, k, n, l, m) and their roles; the appendix proof uses several labels that can be hard to track, especially in the PROMPT and STRONGTEST cases.","section":"Throughout"}],"recommendation":"reject","confidential_remarks":"The paper has a genuinely interesting core calculus and the restricted TINI statements may be salvageable. The main reason for rejection is the mismatch between the advertised contribution and the actual content: the abstract claims a probabilistic whole-calculus theorem and Lean-verified proofs, while the body proves a deterministic, restricted TINI with an incomplete appendix proof and no Lean artifacts. The AgentDojo benchmark claim is also unsupported. These are load-bearing issues, not presentation issues. If the authors add the missing assumptions, complete the proof, provide the Lean formalisation, and rewrite the abstract to match the restricted deterministic result, a resubmission could be worthy of serious consideration."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Read the arXiv paper. My short version: the calculus is a real contribution, and the TINI theorem for the three restricted fragments appears novel. The paper as it stands is not ready, because the abstract states claims the body does not support. The reader's reject is defensible; I'd call it 'major revision required' rather than 'reject', because there is something worth saving.\n\nWhat's actually new: LLMbda is, as far as I know, the first lambda calculus that combines LLM generation, conversation fork/clear, and dynamic labels. The treatment of label testing is genuinely useful: the counterexample showing that unrestricted tests break TINI in multi-level lattices, and the assert/strong-test variants, plus the no-high-upgrade rule on conversations, are a clear step beyond FIDES's fixed schemas and the earlier lambda-calculus languages that ignore security. The big-step semantics are precise enough to prove something real, and the inductive proof strategy is standard and appears sound, modulo the gaps below.\n\nThe soft spots are real and load-bearing. First, the abstract says 'probabilistic noninterference' and 'Lean proofs'; the body gives deterministic TINI for three sublanguages, not the whole calculus, and there are no Lean artifacts. The paper's own Section IV shows a counterexample for the whole calculus, so the abstract is simply wrong. Second, the proof sketch in Appendix A relies on an unstated 'serialisation assumption': in the PROMPT case, from v0 ~_k v1 you need erase_n(v0)=erase_n(v1) to get identical prompts. That property of serialise is not in the semantics definitions, and if serialise formats differently-labelled subterms differently, the noninterference proof collapses. Lemma 2 is stated but not proved; it looks plausible for a reasonable erasure function, but the paper doesn't pin it down. Third, the AgentDojo benchmark claim (1296 attacked runs, utility comparison against CaMeL) appears only in the abstract, with no methodology, no table, no code. That claim should have been in the body or not made.\n\nDon't get me wrong: the deterministic framework is likely salvageable. The fix is explicit assumptions about serialise and parse, the actual erasure lemma, and honest rewriting of the abstract. The Lean claim should only stay if the files appear.\n\nWho is this for? Researchers in PL and security who want a formal foundation for prompt-injection defenses. It deserves peer review, but the review should be with the expectation of major revision. I would send it out.","headline":"The calculus is the contribution; the abstract is the liability.","tokens_in":27672,"tokens_out":2366,"would_cite":true,"duration_ms":24449,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68N18","68Q60","68M25"],"pacs":[],"model":"deepseek-v4-flash","headline":"A lambda calculus with labelled conversations makes prompt-injection defence provably sound.","keywords":["prompt injection","information flow control","lambda calculus","noninterference","AI agents","conversations","dynamic labels","LLMbda"],"falsifier":"Feed two values that are indistinguishable at level k but differ only in subterms labelled above k through the interpreter's serialise path and compare the resulting prompts; if the prompts are not identical, Theorem 1 fails. A simpler end-to-end check: run a qualifying program twice with only a {U}-labelled input changed and look for any observable difference in a {S}-labelled output or conversation.","tokens_in":26779,"feed_emoji":"🦙","tokens_out":6540,"duration_ms":64288,"temperature":0.7,"pith_summary":"The paper tries to establish that the core of agentic LLM programming—prompt-response conversations, forking, clearing, and code generation—can be captured in a small untyped lambda calculus with dynamic information-flow labels, and that this calculus satisfies a formal noninterference theorem. That would matter because today's strongest prompt-injection defences rely on provenance and separation of duty but lack a rigorous semantic foundation; here, isolation becomes ordinary program structure and reclassification becomes an auditable construct. The central result, Theorem 1, proves termination-insensitive noninterference for three classes of programs, the most usable of which replaces unrestricted label tests with assertion and strong-test primitives that still allow policy checks. On a banking benchmark, an agent built in the calculus with enforcement always on matches the utility of a leading dual-LLM defence and resists all but two of 1296 attacked runs.","feed_headline":"Prompt-injection defence gets a provably sound calculus","feed_subtitle":"Labelled conversations let agentic LLM programs prove that untrusted data cannot alter trusted decisions.","key_machinery":"The load-bearing mechanism is the labelled conversation: a big-step semantics with judgements pc ⊢ C, e ⇓ C′, V where pc is the program-counter label and C the labelled history. The @ rule serialises the erased value of e, appends it to the conversation, and parses the model's deterministic response; the erase function strips subterms labelled above the permitted level, and the no-high-upgrade constraint prevents a low conversation from being upgraded from a high context. The n-indistinguishability relation ∼_n and the erasure lemma (v ∼_n v′ implies erase_n(v) = erase_n(v′)) are the proof machinery that carries the noninterference argument. The derived primitives assert_k e and k?? e replac","core_discovery":"LLMbda is an untyped call-by-value lambda calculus whose semantics carries a program-counter label and a labelled conversation history, and adds three agentic primitives: @e asks the LLM a prompt and parses the response, forke runs an expression against a copy of the conversation and discards it, and clear resets the conversation. Every value carries a security label that every reduction propagates, and the semantics enforces a no-high-upgrade discipline on the conversation state. Theorem 1 shows that termination-insensitive noninterference holds for (1) expressions without label tests, (2) expressions using only one non-bottom label, and (3) expressions where tests appear only as assertions","pith_inferences":["If probabilistic model behaviour were admitted, the theorem would likely need a probabilistic analogue of noninterference; the paper points this out, but a concrete probabilistic version would make the guarantee match real nondeterministic sampling.","A practical engineering rule follows from the proof's PROMPT case: the serialiser must be tested for accidental label leakage, since erased values with different hidden labels must serialise to identical prompts.","The conversation-as-state view suggests a generalisation to multi-agent systems where each subagent keeps its own labelled history, with fork/clear as the composition operators between them.","One could imagine a static type system or linter that rejects label tests outside the assert/strong-test forms, turning Theorem 1's third sublanguage into an enforceable programming discipline."],"forward_implications":["Any agent programme written in the calculus inherits the noninterference guarantee, so label-checking wrappers (like a send-email policy that requires trusted subject and body) enforce the intended security policy rather than just hoping the model complies.","The dual-LLM separation pattern becomes a library-level construction—a privileged planner generates code, a quarantined conversation processes untrusted data—and remains covered by the same theorem.","The three sublanguages map a design space: drop label tests, keep a single non-bottom label, or use assertion/strong-test primitives; each is provably safe, so implementations can choose a point on the spectrum.","Because the guarantee is termination-insensitive, the defence blocks data-flow leaks but explicitly permits leaks through termination (e.g., a blocked prompt), which is the same trade-off as classical dynamic information-flow control.","The benchmark result indicates the formal calculus is not just theoretical: with enforcement always on, an LLMbda agent keeps utility on a banking agent task while resisting all but two of 1296 attacks."],"fun_headline_variants":["Provably sound labels stop prompt injection in LLM agents","Lambda calculus gives LLM agents auditable info-flow control","Verified interpreter proves agentic LLM security","The lambda calculus that makes prompt injection impossible"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The noninterference proof assumes, without stating it as a semantic condition, that serialise(erase_n(v)) hides every label difference between n-indistinguishable values; if the prompt serialiser leaks such differences, the theorem's PROMPT case—and with it the whole guarantee—no longer goes through.","fun_headline_variants_meta":{"raw":{"variants":["Provably sound labels stop prompt injection in LLM agents","Lambda calculus gives LLM agents auditable info-flow control","Verified interpreter proves agentic LLM security","The lambda calculus that makes prompt injection impossible"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000468,"raw_usage":{"total_tokens":2230,"prompt_tokens":869,"completion_tokens":1361,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":613,"completion_tokens_details":{"reasoning_tokens":1300}},"tokens_in":613,"tokens_out":1361,"duration_ms":9606,"temperature":1.0,"reasoning_tokens":1300,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T21:24:28.537687+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Feed two values that are indistinguishable at level k but differ only in subterms labelled above k through the interpreter's serialise path and compare the resulting prompts; if the prompts are not identical, Theorem 1 fails. A simpler end-to-end check: run a qualifying program twice with only a {U}-labelled input changed and look for any observable difference in a {S}-labelled output or conversation.","supporting_citations":[],"review_version":1}