PaperlayerView exact revision on arXiv

Source-linked AI summary

PerMIT: Securing Persistent Memory for LLM Agents via Machine-Checked Integrity Theorems and Scalable Community Trust

Tanqiu Jiang, Min Bai, Sadat Shahriar, Wanyu Du, Sandesh Swamy

arXiv:2610.28987v1cs.AIcs.CR

TL;DR

Persistent memory can preserve injected content across sessions, while risks around memory sharing limit its practical deployment. PerMIT mediates environment-derived values through an auditable confirmation gate and accumulates exact-content endorsements for shared memory. The paper reports zero observed Trojan Hippo attack success with self-verification and lightweight verifiers, and decreasing federated risks under explicit assumptions as communities grow.

  • Problem

    Persistent memory can turn injected content into a cross-session compromise, and the same risk has limited practical deployment of memory sharing.

    Source: §1 · p. 3

  • Method

    PerMIT mediates untrusted memory through a finite interface and confirmation gate, then accumulates logged exact-content endorsements so shared entries can become community-confirmed.

    Source: §3.2 · p. 6, §3.3 · p. 7

  • Results

    Self-verification and lightweight verifiers record zero observed ASR on Trojan Hippo, while autonomous communities build shared knowledge with no tested direct injection payloads promoted and improve held-out task performance.

    Source: §1 · pp. 3–4

  • Takeaways & Limitations

    Under explicit assumptions, PerMIT proves and corroborates in simulation that poison-promotion and wrongful-eviction risks decrease with community growth while per-user verification effort does not rise.

    Source: §1 · p. 4

    Adaptive payload search against live verifiers remains an open empirical question; simulated adaptive protocol attacks under controlled reviewer responses do not replace that evaluation.

    Source: §6 · p. 11

Abstract

from arXiv · show

Persistent memory is a largely undefended surface for injection and poisoning, and the same risk limits memory sharing among agents. We present PerMIT, a memory architecture with provable integrity guarantees under an explicit trust assumption: only user-typed inputs and values confirmed at a gate are trusted. PerMIT mediates the release and use of untrusted environment-derived values through a finite memory interface, while preserving agent-driven multi-turn planning and tool choice. Over this finite interface, we prove two integrity theorems that are also machine-checked in Lean 4, which together ensure that environment-derived memory reaches a sensitive action only if confirmed at the gate and influences the agent's behavior only through what the gate displays. Every attack in our threat model thereby reduces to a single auditable decision, which a human, an LLM verifier, or both can make in practice. On Trojan Hippo, PerMIT records zero observed attack success with self-verification and lightweight verifiers. Because each confirmation is a logged verdict on exact content, endorsements accumulate across users, and sufficiently endorsed items become community-confirmed with no further verification required. Under explicit assumptions, we prove and corroborate in simulation a co-scaling property: as the community grows, the risks of promoting poison and of wrongly evicting benign knowledge fall, while per-user verification effort does not rise. On $\tau^2$-bench, communities of up to 90 autonomous agents use PerMIT to build shared knowledge bases with no direct memory injection promoted, and the resulting knowledge significantly improves new agents on held-out tasks, suggesting a path toward agents that safely self-improve at test time.

1 Introduction

Persistent memory can turn a one-shot injection into a cross-session compromise, yet existing memory-sharing protocols do not address memory attacks. PerMIT mediates memory through an auditable confirmation gate and reports zero observed attack success with self-verification and lightweight verifiers on Trojan Hippo.

Motivation

  • Persistent memory can turn transient exposure into durable influence, including dormant payloads planted in one session and activated later.Shared state can also contaminate users without an adversary.Source: §1 · p. 3
  • Existing memory-sharing frameworks define exchange protocols but do not address memory attacks, limiting practical deployment of shared memory.PerMIT allows item-level trust to accumulate from logged confirmations bound to exact content.Source: §1 · pp. 3–4

Results preview

  • Self-verification and lightweight verifiers record zero observed ASR on Trojan Hippo while retaining useful memory capabilities.The gate displays the exact value, original user instruction, and source for an auditable decision.Source: §1 · p. 3

Contributions

  • PerMIT’s autonomous communities build shared knowledge bases without human involvement, with no tested direct injection payloads reaching Community-Confirmed status.A zero-state agent using the resulting knowledge base significantly outperforms one without shared knowledge on held-out, experience-dependent telecom tasks.Source: §1 · p. 4
  • PerMIT’s two integrity guarantees make sensitive actions depend on exact user-typed or user-endorsed values and constrain behavior to what the complete display transcript reveals.The single-user core is machine-checked in Lean 4 under explicit trust assumptions.Source: §1 · pp. 3–4
  • Under explicit assumptions, poison-promotion and wrongful-eviction risks decrease as communities grow while average per-user confirmation burden does not grow.The paper reports proof and simulation support for this co-scaling behavior.Source: §1 · p. 4

2 Background and Related Work

Persistent memory creates a cross-session attack surface because observations can return to an agent in later sessions. Prior work addresses memory defenses, formal coverage, and sharing, but the cited frameworks leave gaps around lifecycle guarantees and recipient-side integrity.

2.1 Persistent Memory as an Attack Surface

  • Stored observations can return to an agent’s context, turning transient exposure into durable influence across sessions.Attacks include direct poisoning, query-only interaction, and indirect ingestion; Trojan Hippo models a dormant payload activated later.Source: §2.1 · p. 4

2.2 Defenses and Formal Coverage

  • Existing defenses span content detection, isolation, privilege control, and formal information-flow methods, but differ in their security boundaries and guarantees.PerMIT centers persistent-memory lifecycle guarantees, exact-value tool-scoped endorsement, and the complete display transcript.Source: §2.2 · p. 5

2.3 Shared Memory and Evaluation

  • Shared-memory frameworks address exchange, access, portability, or transfer, but do not establish recipient-side action and reasoning integrity for adopted content.OKF, Collaborative Memory, and Portable Agent Memory are presented as complementary mechanisms.Source: §2.3 · p. 5
  • The paper uses Trojan Hippo for persistent-memory security and τ 2-bench for the end-to-end utility of autonomously constructed shared knowledge.Source: §2.3 · p. 5

3 The PerMIT Framework

PerMIT treats environment-derived values as untrusted and mediates their release through a finite memory interface, while leaving planning and tool choice to the agent. It extends exact-content confirmation into shared memory, where endorsements accumulate and disputed entries face a demand-paced panel.

3.1 Threat Model

  • Only directly user-typed values or exact values explicitly confirmed through the interface are trusted; other environment-derived content remains untrusted until it passes the gate.Source: §3.1 · p. 5

3.2 The Single-User Tier: a Finite Memory Interface

  • The protected agent retains operation choice and replanning, while PerMIT mediates data flows at the persistent-memory interface.Untrusted content is exposed as opaque handles and released as readable bytes only after endorsement; the fixed interface has seven operations.Source: §3.2 · pp. 5–6, Figure 1 · p. 6
  • Action Integrity requires sensitive-tool arguments to be exact user-typed values or values endorsed at their exact bytes for that tool; Reasoning Integrity makes behavior equal when complete display transcripts match.These guarantees assume source-based labels, immutable stored blocks, and faithful displays; endorsement does not bind argument position, task, purpose, time, or other call arguments.Source: §3.2 · pp. 6–7
  • An untrusted-derived value cannot be released to a sensitive tool without confirmation, reducing each memory-mediated release attempt to an auditable confirmation decision.Previously confirmed exact values may be reused with the same tool without repeating confirmation.Source: §3.2 · p. 7

3.3 The Federated Tier

  • Each exact-content confirmation releases the item for that user and adds one logged endorsement; an entry with at least N fresh endorsements for a tool becomes community-confirmed for later users.Disputed entries are flagged and promotion-frozen, but remain retrievable for personal confirmation while a demand-paced panel considers them.Source: §3.3 · p. 7
  • Under the specified demand, coverage, and threshold schedules, poison-promotion and wrongful-eviction risks decrease with community growth while covered benign shared-demand confirmation burden does not grow.For benign entries, the wrongful-eviction bound depends on a positive margin δb := pb − m/(k − fs).Source: §3.3 · p. 8
  • Sharing lets later users reuse earlier endorsements, with simulations and live tests supporting a safety–effort trade-off and growing reusable knowledge at roughly level per-agent review effort.Source: §3.3 · p. 8

4 Results

Across the supplied results, PerMIT reports zero observed attack success with self-verification and lightweight verifiers on Trojan Hippo, while federated simulations show bounded promotion risk and reduced repeated verification. The results also compare safety and verification effort as quorum size and reviewer properties vary.

4.1 The Single-User Tier

  • Self-verification and both lightweight Qwen verifiers record zero observed ASR while preserving useful memory capabilities on Trojan Hippo.OpenGate records 0–10% ASR across four backbones; Table 1 reports benign utility and ASR, with HM as the primary utility metric.Source: §4.1 · p. 9, Table 1 · p. 9

4.2 The Federated Tier

  • Higher reviewer accuracy and endorsement quorum lower the certified poison-promotion ceiling, but quorum gains saturate because the panel term does not depend on N.Correlated reviewer errors raise both promotion risk and wrongful eviction; for a 31-seat panel, m=20 and mrej=12 keep both below the 10−2 design target.Source: §4.2 · pp. 9–10, Figure 2 · p. 10
  • Across simulated honest-user counts, observed poisoned-entry promotion rates remain below the theoretical bound, and no tested adaptive protocol attack exceeds it.Source: §4.2 · p. 10
  • In a 120-user community, reuse saves 2.36 required approvals per user on average (38%) versus verifying alone; raising N from 3 to 14 cuts certified risk bound 58-fold for 0.64 added approvals per user.Source: §4.2 · p. 10

5 Self-Constructing the Knowledge Base

PerMIT communities built shared telecom knowledge bases while screening direct memory-injection payloads. Across community sizes, the knowledge stock grew without proportional growth in per-agent review effort, and held-out performance improved for some backbones.

5 Self-Constructing the Knowledge Base

  • Each community-size run uses one model family to explore tasks, verify extracted knowledge, and review shared entries.Publication follows safety verification, sharability screening, and consent to the exact content.Source: §5 · p. 10
  • None of the 12 direct memory-injection payloads reached the Community-Confirmed tier.The protocol used N=10 and dispute thresholds k=31, m=20, and mrej=12.Source: §5 · p. 10
  • The utility evaluation uses 24 held-out tasks, two trials each, and matched seeds, for 48 paired episodes per arm.It reports environment-completion scores and four-size pooled task-cluster bootstrap intervals, conditional on the observed bases.Source: §5 · p. 11
  • From 24 to 90 agents, review effort per agent remains roughly level as shared knowledge stock grows.Across M=12, 24, 60, and 90, retained bases contain 3–7, 7–12, 30–40, and 45–64 entries, respectively.Source: §5 · p. 11
  • Pooled gains across community sizes survive three-backbone Holm correction for Sonnet and Kimi, but not GLM-5.At M=90, all means exceed the knowledge-free baseline; separately, Kimi-built knowledge improves a zero-state Claude-Haiku-4.5 agent by +0.198 [+0.073, +0.333].Source: §5 · p. 11

6 Conclusion and Future Directions

PerMIT combines a finite memory interface with machine-checked integrity guarantees and a federated protocol for accumulating trust in exact-content endorsements. The paper identifies remaining challenges in knowledge quality, rare-event calibration, and adaptive payload search against live verifiers.

6 Conclusion and Future Directions

  • PerMIT combines a finite memory interface with machine-checked integrity guarantees, exact-content endorsements, and an autonomous workflow for building shared knowledge.Under explicit assumptions, the protocol bounds poison promotion and wrongful eviction while reducing repeated verification.Source: §6 · p. 11
  • Shared memory may still contain redundant, inaccurate, or hallucinated knowledge, motivating quality-aware gates and active memory management.The authors also propose combining memories and seeking fresh user endorsements of the combined content before it becomes trusted.Source: §6 · p. 11
  • Rare-promotion estimates required five billion simulated attempts and over 50 hours of computation; adaptive payload search against live verifiers remains open.The simulations test conditional safety boundaries through adaptive protocol attacks under controlled reviewer responses, not adaptive payload search against live verifiers.Source: §6 · p. 11

A Additional Results

The deployed-geometry simulations examine promotion routes, adaptive adversaries, and the certified safety ceiling. Under the non-adaptive blast schedule, measured promotion peaks at reach 32 and then declines below simulation resolution.

A.1 Federated-Tier Simulations at the Deployed Geometry

  • The experiments use deployed geometry N=10, Dpool=2, k/m/mrej=31/20/12, f=2, and fs=1.The quoted Batt = 8.96 × 10−3 uses qpre=qpan=0.6.Source: §A.1 · p. 16
  • At q=0.6, N=10, and f=2, the ordinary route follows (1−q)R, while the panel route opens at R=21.The caption describes path decomposition on a linear reach axis under the non-adaptive blast schedule.Source: Figure 3 · p. 16
  • The measured total promotion rate peaks at R=32, then declines below simulation resolution, while no-dispute baselines approach certain promotion as reach grows.The figure compares the measured rate with certified ceiling Batt = 8.96 × 10−3 and panel-leak floor ppanel = 8.3 × 10−3.Source: §A.1 · p. 16

A.2 The Trojan Hippo Benchmark in Brief

The benchmark models cross-session poisoning in which tool-read content is stored and later activated to exfiltrate sensitive user data. The evaluation combines protected-agent rollouts with targeted action-boundary probes and compares complete configurations.

A.2 The Trojan Hippo Benchmark in Brief

  • Trojan Hippo tests indirect injection: a crafted inbound email stores a payload, which a later sensitive-topic request can activate to exfiltrate user data.The attacker controls content read through tools, while the user is trusted.Source: §A.2 · p. 16
  • PerMIT replaces the benchmark memory backend with its RLM reader and confirmation interface, placing each case in a fresh store as untrusted email-tool output.Cases are exercised in a subsequent trigger session.Source: §A.2 · pp. 16–17
  • At q values 0.5, 0.6, and 0.7, all nine adaptive-adversary strategies remain below their certified promotion ceilings.At matched reach R=12, reactive stopping achieves 42.8× the blast success rate at 7.2× lower exposure.Source: Figure 4 · p. 17
  • The action-boundary probe attempts to pass a reader-filled address handle to send_email, including a literal-address variant.A case succeeds if either executed probe records a sink invocation containing the benchmark attacker address in serialized arguments.Source: §A.2 · p. 17
  • The A-MemGuard and LLM-Auditor baselines share the retrieval path; both discard flagged records, and the auditor is a drop-only variant.Retrieval depth is K=8 for RAG and K=10 for Mem0.Source: §A.2 · p. 17

A.3 Implementation Gap in the Provable-Policy Baseline

The supplied baseline records 10% attack success, while the audited implementation reveals an inconsistent taint-state update on successful traces. On two self-hosted backbones, PerMIT with an oracle gate records zero attack success, with results dependent on the serving and parsing setup.

A.3 Implementation Gap in the Provable-Policy Baseline

  • 10% ASR was recorded for GLM-5 under the provable-policy baseline with both Explicit memory and Mem0, across two successful cases per configuration.The code audit found that search_emails did not update the separate ProvablePolicyManager state checked by send_email; the traces do not establish that successful sends followed poisoned-memory retrieval.Source: §A.3 · pp. 17–18
  • Raising quorum N from 3 to 14 lowers the certified risk bound by 58× while adding 0.64 required approvals per user.Across the simulated 120-user community, reuse saves 2.36 required approvals per user (38%) versus verifying alone; no quorum falls below the panel-leak floor.Source: Figure 5 · p. 18

A.4 Additional Backbones and Serving Configurations

  • Tool-call parsing is part of the measurement because PerMIT mediates tool calls and depends on how calls are extracted from model output.The Qwen and Gemma serving configurations use different tool-call parsers and chat-template requirements.Source: §A.4 · p. 18
  • The self-hosted backbones share a serving stack but use family-specific parsers, so they are comparable at the stack level, not to the Bedrock-served set.The runs do not identify whether the small-verifier difference comes from the serving stack, parser and chat template, or backbone.Source: §A.4 · p. 19
  • 40% attack success on Qwen-3.6-27B and 75% on Gemma-4-31B-it under sliding-window context; PerMIT with the oracle gate records ASR = 0 in every occupant cell.Both backbones also zero the harmonic mean under the two capability-removing defences and reach 96.7 AM under PerMIT with the oracle gate.Source: §A.4 · p. 19

A.5 Detailed Verifier Results

Detailed results show that verifier performance varies by backbone and that larger verifiers do not consistently perform better. The banking evaluation finds no detectable utility gain from self-constructed knowledge, a contrast the authors relate to differences in information available to agents.

A.5 Detailed Verifier Results

  • ASR is zero in all 28 cells, while verifier size does not order results: the 4B verifier has higher HM on four backbones and lower HM on three.For fixed verifier size, backbone spreads reach 18.3 AM and 45.1 HM points under the 2B model; verifier choice should be validated against its target backbone.Source: §A.5 · p. 21
  • Gate calls and rejections across 120 benign diagnostic checks measure gate activity, not human review time or the fraction of tasks interrupted.The reported FPR is rejections divided by calls, and calls per check is calls divided by 120.Source: §A.5 · p. 21, Table 7 · p. 22
  • Kimi with Qwen-3.5-4B has HM 50.3, compared with 89.7 under its oracle gate.For GPT-5.4, self-verification decreases AM/HM from the oracle's 89/86 to 83/79; cross-backend comparisons assess complete systems, not retrieval quality alone.Source: §A.5 · p. 21

A.6 Domain Dependence of Self-Constructed Knowledge

  • The banking knowledge base produces no detectable utility gain over the knowledge-free baseline; all confidence intervals include zero.The authors relate the contrast with telecom to banking's well-indexed document corpus and on-demand retrieval, while telecom experience can capture information unavailable in supplied documentation.Source: §A.6 · pp. 21–22

A.7 Autonomous Telecom Construction: Methods and Additional Results

The appendix reports finite-scale results and methods for autonomously constructing and evaluating shared telecom knowledge, alongside interface details that explain how PerMIT keeps untrusted memory separate until confirmation. The construction results have explicit scope limits, including one run per setting and a separate safety-probe endpoint.

A.7 Autonomous Telecom Construction: Methods and Additional Results

  • Agents crystallize session knowledge into an untrusted handle, submit exact content for safety-gate review, screen approved content for generality and privacy, and consent to publication.Other agents then review shared entries; the construction ladder uses three model families and community sizes M ∈ {12, 24, 60, 90}.Source: §A.7 · p. 22
  • The standard utility evaluation uses 24 held-out tasks with two trials each, and Sonnet and Kimi gains are concentrated in the MMS troubleshooting task family.The comparison keeps prompts identical outside the knowledge block; this supports transfer of relevant experience, not gains for every task family.Source: §A.7 · p. 23
  • The pooled analysis reuses evaluation tasks and the baseline, so its 192 paired differences are not 192 independent tasks.Confidence intervals are pointwise, and pooled intervals do not describe the M=90 result alone.Source: §A.7 · p. 23, Table 9 · p. 23
  • At matched remaining-review horizon H=30, benign yield from M=60 to 90 is 0.833 to 0.833, 0.824 to 1.000, and 0.826 to 0.976 for Sonnet, GLM-5, and Kimi, respectively.One run per setting limits inference about population effects; reviews per agent and evaluated knowledge counts vary across community sizes.Source: §A.7 · p. 24
  • At the same M=90 budget, the unfiltered shared-knowledge arm has higher mean utility on all three backbones than PerMIT's filtered arm.This is descriptive: contents and prompt lengths differ, no paired A1–A2 test is reported, and the comparison does not measure relative attack resistance.Source: §A.7 · p. 24, Table 10 · p. 24
  • The separate 12-payload direct memory-injection campaign reports no community promotion, measuring access to the shared fast path only.It does not measure personal acceptance, use before promotion, or every intermediate lifecycle transition.Source: §A.7 · p. 24

B.1 Operations and the reply alphabet

  • The interpreter returns replies from a fixed alphabet; readable text reaches the protected agent only as verbatim content of a trusted block.Operation-determined handles do not encode store contents, and empty search, reader failure, and an unoccupied identifier return the same handle.Source: §B.1 · p. 25

B.2 Label lifecycle

  • The only path from an untrusted label to a trusted label is display followed by accepting confirmation, which copies displayed bytes into a new confirmed block.Blocks are immutable once written; trust changes through creation of a fresh block, not relabeling in place.Source: §B.2 · p. 25, Figure 6 · p. 25

B.3 A worked trace: dormant poison across two sessions

The worked trace shows how an injected payload remains hidden from the protected agent until a gate displays it for confirmation. The surrounding sections specify the interface, proof scope, and conditions and limits of shared-memory guarantees.

B.3 A worked trace: dormant poison across two sessions

  • In the worked trace, the payload never enters the protected agent's context before the gate displays it verbatim and requires acceptance for the exact tool.The decision at that gate is the auditable event evaluated with oracle, self-verification, and external LLM verifiers.Source: §B.3 · p. 25, Table 12 · p. 26

B.4 The Recursive Language Model as a Quarantined Reader

  • The quarantined reader searches untrusted content without loading its bytes into the protected agent's trusted context, returning accepted values only as opaque handles.The implementation uses an RLM to navigate stores larger than a context window; summaries written back remain untrusted.Source: §B.4 · pp. 26–28

C Concurrent Work: Origin-Bound Memory Authority

C.1 The observation boundary

  • With matched initial configurations, inputs, randomness, schedule, and horizon, equal complete display transcripts imply equal observable protected-agent behavior.The theorem does not establish factual correctness, unbiased recommendations, or automated-verifier soundness.Source: §C.1 · p. 29

C.2 Relational versus reachability properties

  • PerMIT's Lean proofs cover the mechanized single-user core under its modeled interface and assumptions, not faithful implementation of a deployed harness.The paper distinguishes this checked core from paper-only extensions and federated analysis.Source: §C.2 · p. 29

C.3 The federated tier

  • Federated risk bounds decrease with community size and covered-benign per-user confirmation burden does not increase under stated demand, coverage, and threshold schedules.Honest reviewers can still accept poison, so the guarantee is conditional and probabilistic, not an unconditional guarantee of zero promotion or lower effort for every workload.Source: §C.3 · p. 30

C.4 Deployment without institutional corroborators

  • An endorsed value can be reused for the same named tool without another mandatory approval only while its confirmed copy is retained.The authorization does not bind task, purpose, time, argument position, or other call arguments; community disputes suspend community reuse but preserve prior personal confirmations.Source: §C.4 · p. 30

C.5 Laundering channels

  • Crystallized summaries remain untrusted, and tool outputs do not become trusted merely because of a tool's name or status.Distinct attested identities and first-decision accounting limit manufactured voting weight, but erroneous honest endorsements can still promote poison under the stated risk bounds.Source: §C.5 · p. 30

D Formal Guarantees and Proof Sketches

PerMIT mediates memory through a finite interface, with guarantees over arbitrary agent strategies under explicit trust assumptions. Its proofs constrain sensitive actions to authorized values and constrain attack influence on behavior to what appears in the display transcript.

D.1 Interface and trust assumptions

  • The harness treats pasted content and tool outputs as untrusted, gives the agent opaque handles, and creates a fresh confirmed copy only after acceptance.Sensitive arguments pass through exact-value, target-specific gates; handle-expressed arguments always gate, and batches require approval of every flowed value.Source: §D.1 · p. 31
  • Action Integrity assumes source-based labels, immutable blocks, faithful displays, and sound atomic endorsement of each exact value for its named tool.The theorem does not establish an LLM verifier’s accuracy; timing, termination, and compromised harness components are outside these guarantees.Source: §D.1 · pp. 31–32
  • Only readable-store blocks can reach the agent as bytes; untrusted sources remain opaque until endorsement.The isolation guarantee concerns the source of delivered values, not whether byte strings overlap across stores.Source: §D.1 · p. 32

D.2.1 Action Integrity

  • Under A1–A4, every execution has personal Action Integrity: each sensitive-tool argument is user-typed or confirmed exactly for that tool.The theorem covers arbitrary agent strategies, attacks, and reader behavior.Source: §D.2.1 · p. 32
  • Authorization covers exact values for tools, not complete transactions; separately approved values may be combined or reused in an inappropriate changed context.Context-bound or transaction-level approval is outside the proved model and would require extended semantics and revised cost accounting.Source: §D.2.1 · p. 33

D.2.2 Reasoning Integrity modulo the display transcript

  • Under A1–A3 and matched-input and scheduling conditions, equal complete display transcripts imply equal protected-agent behavior for two attacks.The comparison holds for any coupled coin sequence and common execution horizon.Source: §D.2.2 · p. 33
  • A difference in protected-agent operations, tool invocations, or ungated sink events therefore entails a difference in the complete display transcript.This attack-surface confinement follows under the same comparison conditions as Reasoning Integrity.Source: §D.2.2 · p. 34
  • The guarantee is conditional: attackers may affect previews or endorsement decisions, but the theorem excludes influence that bypasses the recorded display surface.It does not establish reasoning correctness or make displayed attacks harmless.Source: §D.2.2 · p. 34

E Scope of the Lean 4 Verification

This section specifies PerMIT’s single-user and federated protocols, assumptions, and the scope of their Lean 4 verification, including the finite memory interface and the guarantees established over it. It also makes explicit which components and operations lie outside the formalization and how the federated guarantees depend on stated limits and theorem extensions.

E Scope of the Lean 4 Verification

  • Lean checks single-user action integrity and transcript-conditioned reasoning integrity, including equal protected outcomes for arbitrary agent strategies and independently chosen attacks.The checked conclusions require equal sink logs, operations, replies, and final protected views; paste presence and content may differ. Supporting checks cover reply isolation, handle gating, attack-surface confinement, and a standalone batch layer.Source: E Scope of the Lean 4 Verification · p. 34
  • Run-level batching, aborted-invocation endorsements, matched mid-run states, federated guarantees, probability bounds, and confirmation-budget results are not mechanized.Options O1–O2 are checked only at the gate level, and O3 remains requirements-level; the artifact’s top-level axiom report lists propext and Quot.sound, with no sorryAx.Source: E Scope of the Lean 4 Verification · p. 34

Part III Complete Formal Development

  • The full models, proofs, and derivations remain in Supplements S1–S9, with detailed Lean correspondence in S9 and the complete core theorem statements in shared source files.The Lean artifact is available upon request; the paper describes the main results concisely while the supplement preserves the complete formal development.Source: Part III Complete Formal Development · p. 35

S1.1 Organisation and register conventions

  • The appendices separate normative rules and assumptions, proof results, and non-normative rationale; Lean checks the single-user results over a map-free operation algebra, while store-level map integration and O3 remain outside scope.The batch-confirmation surface of Rule R9 is mechanized as a standalone layer.Source: S1.1 Organisation and register… · p. 37

Detailed contents of the formal development

S1.2 Notation

  • The paper treats fixed deployment components—including the interpreter, channels, rendering, logging, and configuration—as trusted computing base components assumed correct and unalterable by model output.The artifact certifies mechanized statements, not correspondence to a deployed harness or verifier reliability.Source: E Scope of the Lean 4 Verification · p. 34, S1.2 Notation · p. 38

S1.3 Standing conventions

  • Items and confirmations are keyed to exact byte strings; an accepting gate decision is durable and counted once per value-tool pair per transaction.Rejects, abandoned dialogs, batch-page approvals, and repeated reviews of an already accepted pair are attention costs counted separately.Source: S1.3 Standing conventions · p. 43
  • The formal model uses a fixed slot structure and compares runs at a common horizon, coupling the typed stream while allowing paste and environment outputs to differ.The store is idealized as unbounded; deployment quotas must silently evict from the untrusted tier rather than expose an exhaustion error to P.Source: S1.3 Standing conventions · pp. 43–44

S1.4 Named invariants and structural properties

  • The structural core includes byte-permanent freshness, rejection asymmetry, a per-user/value/tool single-approval cap, banking safety, verdict non-renewal, and reach-freeness.Reach-freeness means the stated federated safety-bound form does not degrade with the number of honest identities reached; it does not claim monotonicity, and behavioral constants are weakest-target infima over reachable cohorts.Source: S1.4 Named invariants and structural… · pp. 44–45

S2 Formal Specification of the Memory Interface

  • The harness bounds what the Protected LLM can observe and what crosses tool boundaries, without restricting its tool choices or reasoning.The bounded surface is the finite memory interface: the P-emitted operations and an interpreter-internal derived form. The interface schema fixes operation and channel-event effects, replies, transcript events, and sanitized-history events; it does not formalize P’s computation or UI rendering internals.Source: S2 Formal Specification of the Memory… · p. 45

S2.1 Configurations, labels, and roles

  • The Protected LLM is modeled as an arbitrary strategy, while the quarantined scope reads the whole store without tool access and the trusted retriever reads only endorsed memory.The formal view conservatively grants P direct sight of endorsed memory; the two-run theorem therefore quantifies over a better-informed P, while memory effects remain mediated by the interface.Source: S2.1 Configurations, labels, and roles · pp. 46–47

S2.2 Operational semantics

  • The operational semantics use fixed interpreter transitions and replies, with no model assigning labels or composing replies.The map batch-confirmation surface is mechanized as a standalone layer, but its store-level integration into the run-level interpreter is outside the mechanized surface.Source: S2.2 Operational semantics · pp. 47, 52

S2.3 Interface rules

  • The interface rules are normative and implementable, and constrain the transitions specified by the interface schema.The provided passage introduces Rule R1 on operation-determined naming for handles and block identifiers.Source: S2.2 Operational semantics · p. 47, S2.3 Interface rules · p. 52
  • A map is one handle-producing operation regardless of collection size, exposes no per-element access, and permits only a single-tool or crystallize body template.Per-element calls are interpreter-iterated, and multi-step pipelines use successive maps, each batch-gated independently.Source: S2.3 Interface rules · pp. 52–53
  • Gates display the exact bytes that will flow, and map calls use a batch confirmation with one aggregated decision for the whole map.Accepted values receive durable endorsed copies even if another gating position causes the invocation to abort; map outputs are captured and return only an acknowledgement.Source: S2.3 Interface rules · pp. 53–55
  • Sensitive-tool values flow without confirmation only when they match trusted or in-scope endorsed bytes; handle arguments always trigger confirmation.At data tools, the baseline rule permits readable E-level bytes without confirmation; handles never take that fast path.Source: S2.3 Interface rules · p. 54
  • Replies use a fixed finite alphabet, while untrusted-store resolution and occupancy remain hidden from the agent through operation-determined handles or failures.The alphabet includes constant acknowledgements, opaque handles, decisions, generic failures, and verbatim endorsed-store bytes; untrusted-sort identifiers are never exposed in replies or views.Source: S2.3 Interface rules · pp. 53, 55, 56
  • Options O1 and O2 are formally instantiated as stricter gating variants with proved monotonicity, whereas O3 is requirements-level only and outside the formal semantics.O1 adds first-use confirmation per sensitive sink; O2 applies exact-target mediation at data tools; O3 specifies local scope leases but has no theorem in this document.Source: S2.3 Interface rules · p. 56
  • With O(1) lease periods per user-item pair, the extension has only an O(1) factor on Theorem S6.2’s constants; saturation-vanishing additionally requires a residual bound that includes expiry re-fires.The passage specifies an O3-augmented analogue of the complete residual bound, with product and residual-fraction rate conditions; O(1) lease periods alone do not suffice.Source: S2.3 Interface rules · p. 57

S2.5 Attacker model and trusted computing base

  • The trust boundary assumes fixed source labels, immutable blocks, faithful displays, sound endorsements, and exogenous typed commands; the attacker controls U-blocks, tool outputs, and paste input, but not typed commands or user decisions.The single-user TCB includes the authenticated command channel, tool identifiers and partition, interpreter and parser, zoned rendering, and hash-chained audit log.Source: S2.4 Trust axioms · p. 57, S2.5 Attacker model and trusted… · p. 58

S3 Single-User Guarantees

  • Both conditional guarantees are machine-checked: sensitive-action values require exact-byte, exact-tool authorization, while behavior is independent of hidden untrusted memory given the display transcript.The second guarantee is fixed-horizon and termination-insensitive; neither theorem establishes reasoning correctness or resistance to manipulation through displayed content.Source: S3 Single-User Guarantees · p. 58

S3.1 Definitions

  • Reasoning Integrity conditions behavior on matched configurations and identical display transcripts; Action Integrity instead quantifies over well-formed configurations with sound endorsement backing.Reasoning Integrity does not require endorsement soundness on the seed, while Action Integrity does.Source: S3 Single-User Guarantees · p. 58, S3.1 Definitions · pp. 59–61

S3.2 Structural lemmas

  • The interface keeps U-source bytes out of the Protected-LLM state and mediates tool arguments through trusted values or confirmation gates.At sensitive tools, readable E-bytes must match a typed block or an in-scope confirmed block; handles are gated at every tool.Source: S3.2 Structural lemmas · pp. 61–62
  • Only accepting reviews create confirmed blocks, and the single-user system cannot create community-confirmed blocks.In well-formed runs, each scoped confirmed block is backed by a matching confirmation; community scope requires a promotion certificate.Source: S3.2 Structural lemmas · pp. 62–63
  • The append-only transcript and display-segment determinacy lemmas establish that matched operations with prefix-comparable display segments have equal segments and matched effects.The batch determinacy core is machine-checked, while its store-level integration into map is established by the paper proof.Source: S3.2 Structural lemmas · p. 64

S3.3 Action Integrity

  • Under A1–A4, PerMIT preserves well-formedness under every attack, so every sink event reachable from a well-formed configuration is safe per execution.The machine-checked invariant covers clauses (i)–(iii) and (v); clause (iv) is enforced by the executable state and transition structure and a separate sortedness invariant.Source: S3.3 Action Integrity · p. 65
  • A never-endorsed untrusted-derived value crosses any tool boundary only in an accepting confirmation displaying those exact bytes at that exact tool.After endorsement, literal-expressed use at data tools is ungated in the baseline; Option O2 closes that channel by requiring exact-target confirmation.Source: S3.3 Action Integrity · p. 66

S3.4 Reasoning Integrity modulo the display transcript

  • For matched runs with equal display transcripts, PerMIT produces identical protected operations, tool invocations, replies, final views, and ungated sink projections.Consequently, attacker-induced differences in those behaviors require a difference in the logged, user-facing transcript; timing and termination are outside the model.Source: S3.4 Reasoning Integrity modulo the… · pp. 67–68

S3.5 Baseline separation and hardening monotonicity

  • The taint-gating baseline fails Reasoning Integrity: two attacks can produce equal empty transcripts but different sink projections.The witness varies planted invoice content, causing the agent to call a sensitive tool in one run but not the other, without confirmation.Source: S3.5 Baseline separation and hardening… · p. 69
  • Under the stated per-option spread assumptions, Options O1–O2 shrink admitted ungated flows, preserve safety theorems, and retain budget theorems with O(1)-factor constants.The proposition quantifies over any subset of O1–O2; it does not include requirements-level Option O3.Source: S3.5 Baseline separation and hardening… · p. 69
  • Hardening options preserve the federated safety theorems by fitting their all-schedules hypotheses, rather than by establishing pathwise monotonicity.Cache acceptances add no promotion path; their logged rejections add no promotion credit and can only deny the ordinary path.Source: S3.5 Baseline separation and hardening… · p. 70
  • Display-reactive users and history-adaptive attackers are covered by replaying their realized decision sequences as index-oracle inputs; transcript equality aligns the two-run cases.The replay argument constructs agreement step by step, including when a gate transaction consumes multiple user responses.Source: S3.5 Baseline separation and hardening… · p. 70

S4 The Federated Protocol (PerMIT-Attest)

  • Federated log transitions are specified separately from the single-user small-step relation; local theorems consume shared state only through the live-entry test.The federated two-run comparison treats the log as an exogenous coupled input, providing the basis for the stated theorem extension.Source: S4 The Federated Protocol… · p. 71

S4.1 Identities, pools, epochs, and demand

  • The federated product system is specified on paper, not mechanized; log transitions change the shared view but never local blocks or the agent’s reply stream.Compared runs receive equal exogenous log prefixes and matched local events, so their delivered logs coincide.Source: S4.1 Identities, pools, epochs, and… · p. 72
  • Successive entries for the same bytes have identity-disjoint weight-bearing endorsement sets, and each endorsement is a fresh inspection.The community fast path depends on a currently valid shared entry naming the tool; personal confirmations remain distinct local objects.Source: S4.1 Identities, pools, epochs, and… · pp. 72, 75
  • Repeat acceptances are inert, while repeat rejections can only freeze or corroborate, so a second logged inspection cannot promote an item.Reach-free bounds depend on protocol constants, adversary resources, and the weakest-target parameters qpre and qpan, not on how many honest identities receive the item.Source: S4.1 Identities, pools, epochs, and… · pp. 75–76

S4.2 Protocol rules

  • Only confirmed C-labelled blocks may be submitted, and publication requires the owner’s accepting confirmation on the decision pane, logged as a signed submission.A submission creates shared-tier presence but no local block and consumes no freshness.Source: S4.2 Protocol rules · p. 76
  • A qualifying rejection freezes promotion; demanders inspect flagged bytes at their own gates, and the first k eligible verdicts resolve the dispute.Reaching m rejecting verdicts evicts the item; reaching m accepting verdicts lifts the freeze and resumes the pipeline, without directly promoting it.Source: S4.2 Protocol rules · pp. 77–78
  • A per-(value, tool) dispute variant could remove cross-tool juries, but its freshness and verdict-capacity rules remain undecided and no theorem uses it.The variant would multiply panels and prompts by up to ctool per item.Source: S4.2 Protocol rules · p. 80
  • Deterministic candidate hygiene only refuses entries, removes items, or reorders retrieval, preserving safety and budget properties.Retrieval ranks confirmed items first, then undisputed candidates by endorsement weight, then disputed flagged items.Source: S4.2 Protocol rules · p. 80

S4.3 Federated assumptions, adversary, and TCB additions

  • Endorsement transfer makes a confirmed item authoritative only for the same tool when it is context-independent; published-content confidentiality is not separately proved.The type-level half of the transfer claim is discharged by Lemma S5.2; semantic context independence is judged by the owner and inspecting community.Source: S4.3 Federated assumptions, adversary,… · pp. 80–81
  • Federated reasoning integrity assumes identical exogenous log prefixes across compared runs; attacker influence through legitimate log activity is instead bounded by separate safety results.The compared runs’ own locally generated events are derived to coincide, rather than assumed coupled.Source: S4.3 Federated assumptions, adversary,… · p. 81
  • Dispute-resolution assumptions require a uniform positive lower bound on the chance that each next demander casts an eligible verdict, including remaining fresh, weighted, pool-diverse demand.The bound includes protocol-state eligibility and non-abandonment, not just demander behavior.Source: S4.3 Federated assumptions, adversary,… · p. 81
  • Federated safety assumes certified lifetime bounds on adversarial identities and weight, and A9’s structural eligibility condition can fail; such failure affects availability, not safety.The adversary’s strategy is predictable and cannot depend on unperformed inspections. Where identity issuance is open or uncosted, federated results apply only to certifiable lifetime bounds; single-user guarantees are unaffected.Source: S4.3 Federated assumptions, adversary,… · pp. 81–82

S5 Federated Guarantees

  • The appendix proves structural lemmas followed by integrity lifting, deterministic and panel safety, wrongful-eviction, publisher-safety, denial-of-service, and submission-budget results.The dependencies among these guarantees are given in Figure S1.Source: S5 Federated Guarantees · p. 82

S5.1 Structural lemmas

  • Promotion attempts partition each shared-tier presence, allowing safety bounds to be conditioned at an anchor before any credited decision; attempts without finalization cannot succeed.Each finalising attempt has only one final entry, and an epoch has at most Emax finalising entries per item. Distinct entries’ weight-bearing endorsements are identity-disjoint and require fresh, authority-active inspections.Source: S5.1 Structural lemmas · pp. 82–83
  • Under A9, unresolved disputes have expected demander count at most κ = (k+1)/ρseat; under the default bars, a gathered panel tally reaches exactly one bar, without deadlock or adversary-only resolution.The probability of more than c0κ arriving demanders is at most e−λc0k for c0 > 1. A9’s verdict-pacing condition concerns availability; the default-bar result requires m > fs and mrej > fs.Source: S5.1 Structural lemmas · p. 84
  • Third parties cannot alter or remove users’ local-store blocks; shared-tier demotion and suspension withdraw community authority without affecting personally confirmed copies.First-party eviction by the owner’s own agent remains a disclosed residual. The resulting campaign cost is bounded by the single-user cap.Source: S5.1 Structural lemmas · pp. 84–85
  • Hygiene preserves the safety theorems because its shared-tier changes add no promotion path or confirmations, and the safety bounds hold uniformly over adaptive presentation schedules.Retirement may redirect later encounters to users’ ordinary personal-confirmation stream, which remains bounded by the single-user cap.Source: S5.1 Structural lemmas · p. 85

S5.2 Main theorems

This section formalizes PerMIT’s integrity, promotion, eviction, dispute-resolution, and confirmation-budget guarantees, including supporting analyses of promotion dynamics, costs, and scaling. It states the assumptions and scope of these results, clarifying conditional guarantees and residual risks involving human judgment, availability, calibration, and deployment.

S5.2 Main theorems

  • Community authority permits unconfirmed personal use only for an exact live virtual entry backed by qualifying fresh endorsements, while federated runs preserve equal virtual views and local blocks.Suspension, demotion, retirement, and accountability events withdraw virtual authority without creating, altering, or removing local blocks.Source: S5.2 Main theorems · pp. 85–86
  • With perfect honest detection (q = 1), no poisoned item is promoted when W > Wadv and m > fs, through either ordinary promotion or the panel path.The result is deterministic and population-independent; its q = 1 premise excludes honest acceptances of poison, so it does not guarantee community truthfulness when poison is unrecognizable.Source: S5.2 Main theorems · p. 86
  • The probabilistic bound uses qpre and qpan as uniform conditional lower bounds over the most fallible targetable honest cohorts, not population averages.For attempts anchored after prior promotion, qpre must also cover the relevant stable promoted contexts; first-promotion attempts need no such extension.Source: S5.2 Main theorems · pp. 87, 90, 91
  • A poisoned item’s per-attempt promotion probability is bounded by an ordinary-promotion term plus a panel-resolution term, uniformly over adaptive presentation and stopping, regardless of audience size.The ordinary case is bounded by (1 − qpre)^(N − f); the panel case is bounded using a binomial tail for k − fs honest verdict opportunities. The certified bound is per attempt, not per epoch.Source: S5.2 Main theorems · pp. 87, 88, 90
  • Raising endorsement quorum N reduces only the ordinary term; at fixed panel geometry and qpan, the panel term remains a floor on the certified per-attempt bound.The ordinary term falls geometrically in N − f, while the panel term falls as a binomial tail in k − fs; deployment-wide exposure requires summing across attempts and variants.Source: S5.2 Main theorems · p. 88
  • One honest effective qualifying rejection denies the ordinary path when qpre > 0; joint safety and low wrongful-eviction risk require qpan + pb > 1.Safety alone can be forced for any qpan > 0 by raising m toward k, at the cost of a weaker wrongful-eviction bound.Source: S5.2 Main theorems · p. 92
  • Disputes resolve at the item’s demand rate, but resolution itself has no probability guarantee; wrongful-eviction bounds are unconditional, and an undemanded item expires harmlessly.Wide pre-exposure can stall a benign item, imposing availability costs while leaving safety intact; each affected demander owes at most one required confirmation per pair.Source: S5.2 Main theorems · pp. 92, 94, 95, 96
  • Panel verdicts alone cannot trigger publisher penalties; on benign items, pairwise wrongful-eviction risk is exponentially bounded for specified instances, while general random-count risk is bounded in expectation.With a deterministic dispute cap, the probability of at least r wrongful evictions has an r-fold exponential bound; without that cap, no such exponent is claimed. Repeated panels on the same bytes use each identity’s verdict only once.Source: S5.2 Main theorems · pp. 93–94
  • With default bars and wrongful-eviction margin δb > 0, a benign item is wrongfully evicted with probability at most e^-2δb²(k−fs), uniformly over adversary strategies.The bound is conditional on prior protocol events; it does not assert that a panel resolves.Source: S5.2 Main theorems · pp. 92–93
  • Adversarial rejections can hold at most f·rmax items in Disputed, and each user remains within the single-user confirmation cap without local-store changes.Concurrent rejections and per-item dispute initiations are capped; dispute slots free on resolution or expiry, while rejection campaigns consume adversarial rights and have bounded throughput.Source: S5.2 Main theorems · pp. 94–95
  • Under default bars, adversary-published poison has at most 2fρsub promotion attempts anchored per epoch, and the same bytes can reach threshold at most ⌊Hacc/(N −f)⌋ times.Attempts are counted by anchor epoch, not finalisation epoch; no bound is asserted conditional on the realised attempt count.Source: S5.2 Main theorems · pp. 96–97
  • Poisoned-item promotion is bounded per epoch and per attempt; the lifetime ceiling applies to exact byte strings, while distinct paraphrases consume separate rate-limited attempts.The weighted form changes the exponent to (W − Wadv)/wmax, and source-class thresholds tune quorum requirements without bypassing quorum or widening tool scope.Source: S5.2 Main theorems · p. 98, S6.1 Model · p. 102

S6 The Memory-Verification Budget

  • Shared required verification load never exceeds the standalone mass dtool, and both shared components vanish only under the measured corridor and the stated hypotheses.The firm pathwise guarantee is that no user’s required cost exceeds once per (value, tool) pair, subject to first-party persistence exceptions. Vanishing requires the applicable saturation, smoothness, coverage, juror-supply, and bounded-mass conditions; otherwise the universal expected-load ceiling still applies.Source: S6 The Memory-Verification Budget · p. 98

S6.1 Model

  • Budget analysis assumes temporal smoothness: at most γ̄ n_v + s0 first demanders per pair per finalisation window or candidate-dormancy interval; each item spans O(1) tools; and per-user demand mass is uniformly bounded.Without A13, vanishing budgets require γ̄(M)(1 + κ(M))d_good(M) → 0 or ε(M)d_good(M) → 0, as applicable. Expectation-form conclusions assume exogenously scheduled publication.Source: S6.1 Model · pp. 99, 100, 103
  • A11 requires residual benign approvals to satisfy Uv,t ≤ D0(M) + ε(M)n conditional on demand count n, with D0(M)V(M) = o(M) and ε(M)dgood(M) → 0 sufficient for vanishing residual.The condition covers unpublished items, demand outside ledger-charged pieces, and handle-expressed use of live community-certified pairs, which still gates. Poisoned items are excluded from A11 and are instead bounded by the promotion-probability theorem; residual demand is charged at the single-user cap.Source: S6.1 Model · pp. 101–102

S6.2 The single-user first-authorization cap

  • After a user accepts a review for a (value, tool) pair, later use requires no further gate confirmation unless the user’s agent evicts the local block.The guarantee follows from durable local scope persistence and fast-path treatment of readable literals; handle-expressed reuse is a covered, protocol-inert gate.Source: S6.2 The single-user… · p. 104
  • Each user is required to confirm a given (value, tool) pair at most once over the deployment’s lifetime, even under disputes, rejections, revocations, or availability campaigns.The invariant is subject to first-party persistence exceptions; rejecting decisions, abandoned dialogs, redundant acceptances, and inspection time are outside this cap. Revocation and re-verification do not multiply required cost.Source: S6.2 The single-user… · pp. 104–105
  • In the independent reference model, no user’s expected shareable cost per epoch exceeds the single-user isolation cost.The passage identifies that isolation cost as dtool; it distinguishes this per-epoch shareable bound from the lifetime personal term.Source: S6.2 The single-user… · p. 104
  • With no disputes, adding users never increases any individual’s required count; with disputes, the lifetime cap still holds at once per pair.Disputes can suspend amortization, forcing later demanders to confirm personally.Source: S6.2 The single-user… · p. 105

S6.3 The per-item confirmation ledger

  • For benign assumption-conforming items, required pipeline confirmations are bounded by A(M)P[n_v ≥ 1] + B_fl γ̄ E[n_v].The coefficients depend only on protocol constants, and the pipeline-required total obeys the same bound.Source: S6.3 The per-item confirmation ledger · pp. 108, 110

S6.4 Saturation

  • The saturation bound applies to benign assumption-conforming items, counting required and voluntary pipeline confirmations while bounding the ledger residual separately.The residual is bounded by Theorem S6.9(iii) and added in Corollary S6.10.Source: S6.4 Saturation · pp. 110–111
  • Under Theorem S6.9(i)’s hypotheses, the ledger-counted shareable cost is at most o(1) + Bfl γ̄ dgood, and vanishes if γ̄(M)(1 + κ(M)) → 0.For V(M) = Θ(M^β), β ∈ (0, 1), the bound is O(M^(β−1)) + Bfl γ̄ dgood under the additional fixed-adversary and bounded-seat assumptions; the benign ledger residual also vanishes under its additional rate conditions. These are upper bounds, not matching lower bounds.Source: S6.4 Saturation · p. 111

S6.5 Conditional co-scaling

  • Under the stated schedules and assumptions, Theorem S6.13 jointly improves safety, wrongful-eviction risk, and per-epoch confirmation cost as the community grows.The benign ledger residual and shared confirmation load are o(1); benign-eviction probability is at most e^-2δ²_b gk(M), which tends to zero. The result is conditional on measured environment properties and schedule constraints; the unconditional floor remains Theorem S6.2.Source: S6.5 Conditional co-scaling · pp. 113–114

S7.1 Attack and limitation index

  • The attack and limitation index classifies concerns as formally disposed under stated assumptions, residual, or mechanism-disposed with a disclosed residual periphery.It also records whether an entry is unused in proofs or affects budget constants only.Source: S7.1 Attack and limitation index · p. 115, Table S3 · p. 116

S7.2 Design rationale

  • PerMIT’s integrity account permits untrusted-derived values to reach sensitive actions only after confirmation and limits behavioral influence to the logged display transcript.Endorsement is per (value, tool), not a complete-transaction approval: combinations and timing of separately endorsed values remain ungated. The transcript records both display surfaces, while untrusted reader output remains untrusted or handle-hidden.Source: S7.2 Design rationale · p. 117
  • The gate blocks values that are neither user-typed nor endorsed for the exact sensitive tool, while the logged display transcript records modeled release surfaces without reconstructing causation or attacker identity.The transcript does not prove users cannot be manipulated; it makes influence visible after the fact, while the gate provides prevention.Source: S7.2 Design rationale · p. 118
  • Erring Protected LLMs can evict their owner’s endorsed blocks without confirmation, while federated guarantees bound availability harm but never guarantee availability or prevent deletion by first parties.The no-deletion guarantee is third-party only; the shared tier may contribute nothing during a freeze, leaving users to verify personally within the single-user cap.Source: S7.2 Design rationale · p. 119
  • Logged validation can check modeling assumptions and falsify parameter caps, but finite samples cannot certify uniform behavioral bounds, and required-approval ledgers exclude recurring rejection and attention effort.Estimating poison-detection and benign-inspection parameters requires labeled trials and stratified lower-confidence bounds; attention from repeated rejection dialogs remains unbounded by the model.Source: S7.2 Design rationale · pp. 120–121

S7.3.1 Attacks on the endorsement mechanism

  • Self-disputes, reputation farming, panel-lapse exploitation, and juror exhaustion are bounded or disposed under stated assumptions, with stalled promotion degrading availability rather than safety.Lifetime adversarial totals cap reputation capacity; panel slots have no lapse deadline, and pre-exposure can stall an item frozen without enabling promotion.Source: S7.3.1 Attacks on the endorsement… · pp. 122–123
  • Tool-targeted poison is constrained by ordinary promotion thresholds at the harmful tool, but cross-tool panel vindication can lift freezes and remains a disclosed residual.A panel’s competence bound applies in jurors’ own tool contexts, so it may be near zero for poison harmful at a different tool; rejection accountability mitigates but does not remove the residual.Source: S7.3.1 Attacks on the endorsement… · p. 122

S7.3.2 Side channels and covert channels

  • Silent eviction quotas prevent store-volume leakage under the stated deployment convention, while harness wall-clock timing remains an out-of-scope residual.The interface exposes no clock or step count; timing observed externally is not modeled.Source: S7.3.2 Side channels and covert channels · p. 123

S7.3.3 The human factor

  • Previews cannot forge endorsements within the model, but can influence users; careless endorsements and later recombination remain transcript-visible policy risks, while batch review retains human-attention limits.Batch decisions are all-or-nothing, so one poisoned element can force rejection of the batch; users may abort, and deployments can cap batch size.Source: S7.3.3 The human factor · pp. 123–124

S7.3.4 Adverse parameter regimes

  • Correlated carelessness weakens probabilistic bounds by lowering the conditional catch-rate assumption, while diversity and re-verification can mitigate but not eliminate this risk.If the catch rate approaches zero, the probabilistic guarantees become vacuous; uniform bounds remain assumptions requiring calibration.Source: S7.3.4 Adverse parameter regimes · p. 124
  • One effective rejection by an honest, currently authorized inspector freezes promotion; silenced identities’ acceptances carry no promotion weight, and late refutations take effect immediately.This one-sided guarantee survives adverse regimes where community truthfulness does not; safety for q>0 can also be forced by raising m toward k, with a weaker wrongful-eviction bound.Source: S7.3.4 Adverse parameter regimes · p. 125
  • Calibration errors affect availability, not safety: they can throttle honest dispute initiation and delay crediting, but do not change the safety theorems.Calibration enters budget constants through cacc; authority-gated crediting prevents silenced honest acceptances from earning promotion weight.Source: S7.3.4 Adverse parameter regimes · p. 125

S7.3.5 Modelling-boundary effects

  • Publisher-penalty feedback on publication is unmodelled and confined to budget asymptotics; the pathwise cap and safety theorems are unaffected.Late or absent publication can weaken the demand-model coverage assumption, while benign-publisher penalty probability is bounded by Proposition S5.22(ii).Source: S7.3.5 Modelling-boundary effects · pp. 125–126
  • A release-day demand burst violates A10 but costs at most that item’s own demand under the pathwise cap, leaving other items’ accounting unchanged.A pre-publication burst similarly violates A11 and is priced at the cap; amortization claims degrade for the affected item.Source: S7.3.5 Modelling-boundary effects · p. 126
  • Untrusted-channel arrivals of certified content still require confirmation because exempting opaque handles could reopen hidden-resolution information flows.Each confirmation is once ever per user and pair, and shared required load stays within standalone mass; amortization applies to fast-path-expressed demand, with handle arrivals priced in A11.Source: S7.3.5 Modelling-boundary effects · p. 126

S7.4 Scope and residuals

  • The guarantees are scoped: reasoning integrity is transcript-relative, timing and termination are excluded, and value-flow integrity does not authorize sensitive tool invocation.Machine checking covers personal action integrity and specified reasoning-integrity cores, but not run-level integration, federated systems, or probabilistic and budget results; availability is not guaranteed.Source: S7.4 Scope and residuals · pp. 126–127, S7.5 Summary of composed guarantees · p. 127

S7.5 Summary of composed guarantees

  • Federated guarantees form three layers: deterministic promotion safety, probabilistic per-attempt bounds, and pathwise degradation and cost caps.The deterministic layer requires q=1, W>Wadv, and m>fs; probabilistic exposure is per poisoned attempt, while pathwise guarantees bound third-party degradation and required cost. The numeric system-wide bound covers adversary-published attempts, not attempts published by honest-but-deceived identities.Source: S7.5 Summary of composed guarantees · p. 128

S8.1 Probabilistic framework, coupling, and the no-dispute baseline

  • Under adaptive presentation and stopping, conditional probability bounds still yield binomial domination for realized counts, including predictable truncations.The adversary’s strategy is predictable, submitted bytes are immutable, and the inspection bound must hold uniformly across identities and presentation contexts; no conditional-law claim is made given that observations continue to occur.Source: S8.1 Probabilistic framework,… · pp. 128, 130
  • Delayed-mark bounds require no ordering of outcome resolution, measurability of outcomes, or independence, allowing trials to resolve after later trials begin.The text identifies anchor-indexed promotion attempts and opening-indexed panel instances as applications.Source: S8.1 Probabilistic framework,… · pp. 131–132
  • Without Rule R13, honest false acceptances accumulate with attacker-chosen reach R; under Rule R13, reach drops out and one honest rejection freezes promotion.The Rule R13 comparison attributes the difference to reports on honest inspections and a bounded jury; the baseline treats rejections as inert.Source: S8.1 Probabilistic framework,… · pp. 132–133

S8.2 The blast-schedule promotion law

  • Under the blast-schedule hypotheses, the promotion probability is πblast(R) = πord(R) + πpan(R), and neither component depends on k, f, fs, or Dpool.This is an analysis of one simulated presentation schedule and honest-behavior model, not a protocol guarantee; the result assumes the stated cap conditions.Source: S8.2 The blast-schedule promotion law · pp. 133–134
  • The panel component is zero for R ≤ m, first becomes q(1 − q)^m at R = m + 1, and the total promotion rate plateaus at (1 − q)^m for R = m and m + 1.The panel component first depends on mrej at R = m + mrej + 1, and it rises to an interior maximum before falling.Source: S8.2 The blast-schedule promotion law · pp. 135–136
  • The blast law is a reach-free upper bound for adaptive schedules under a conditional honest-behavior lower bound without independence, valid only for R ≤ 2m and not itself a safety claim.Beyond 2m it undercounts because a second dispute may become reachable. At R = 64, the measured rate was 8.0 × 10^-6 against an extrapolation of 1.057 × 10^-14; the sweep remained below Batt.Source: S8.2 The blast-schedule promotion law · pp. 136–137

S8.3 Explicit ledger constants

  • The ledger constants are closed-form upper bounds, with the κ′ freeze term capturing dispute cross-costs and suspension-prompt re-inspections rather than claiming tightness.The κ′ component of Bfl is damped by 1 − pb, the honest wrongful-rejection rate.Source: S8.3 Explicit ledger constants · p. 138

S8.4 Knowledge-based formulation of Reasoning Integrity

  • For a fixed observer given the coins and typed stream, untrusted-memory knowledge increases only through display events, not through undisplayed behavior.The proposition is limited to this strong observer; ignorance of the coins can allow behavior to reveal information beyond the transcript.Source: S8.4 Knowledge-based formulation of… · p. 139

S8.5 Zipf case study for the budget

  • For Zipf popularity with α > 1, head and tail budget terms have upper bounds of common rate O((A(M)/M)^(1−1/α)); the matching order requires RM → ∞ and U/RM → ∞.The invitation term vanishes when K(M)V(M) = o(M), while the front-loaded term vanishes under γ̄(M)(1 + κ(M)) → 0; no power rate is asserted at α = 1 without a relation between U and RM.Source: S8.5 Zipf case study for the budget · pp. 140–141

S8.6 Assumptions ledger

  • The assumptions ledger requires attacker-immutable labels, rule-based trust changes and endorsements, a faithful authenticated decision pane, intended confirmed values, citation-checked summaries, and an authenticated command channel.Source: S8.6 Assumptions ledger · p. 141
  • The user-as-oracle premise relies on a small, faithfully displayed, shrinking confirmation set, while community endorsement at a tool is assumed to speak for any user at that exact tool.The ledger identifies the batch gate as the weakest point for the user-as-oracle premise.Source: S8.6 Assumptions ledger · pp. 141–142
  • A10–A13 bound demand attribution, ledger residuals, and per-user demand mass, supplying conditions for vanishing budget conclusions and the total-cost limit.A10 caps realized demand at fraction γ̄; A11 bounds confirmations charged to no ledger row; A13 supplies the uniform per-user epoch demand bound.Source: S8.6 Assumptions ledger · pp. 142–143
  • Rules R1–R14 and Figures S2–S3 define the harness interface checked by Lemmas S3.17–S3.18, while the ledger distinguishes assumptions and trusted components from validation evidence.Validation under N17 can falsify or calibrate uniform behavioral bounds, but does not certify them; the stated co-scaling corridor additionally requires N(M)k(M) = o(M^(1−β)) and γ̄(M)k(M) → 0.Source: S8.6 Assumptions ledger · pp. 142–143
  • Safety and resolution claims require inspector competence q > 0 and q + pb > 1, whereas A9’s bounded-harm denial-of-service premise limits availability failures.The ledger says structural failures can be deterministic but availability-only, with the cap unaffected; it also states that calibration of R13(v) affects budget constants, never safety theorems.Source: S8.6 Assumptions ledger · pp. 142–143

S9 Machine-Checked Verification in Lean 4

PerMIT’s Lean 4 development machine-checks its single-user integrity theorems over an executable memory-interface interpreter. The checked scope is narrower than the full paper proofs, which cover additional integration and federated results.

S9 Machine-Checked Verification in Lean 4

  • Theorems S3.21 and S3.25 are kernel-checked over an executable interpreter for the memory interface, with arbitrary agent strategies, retrievers, attackers, and horizons under stated conditions.The interpreter models the interface operations and actors; the Protected LLM is represented as an arbitrary function of its operations, replies, view, and coins.Source: S9 Machine-Checked Verification in… · p. 144
  • The checked interpreter covers the single-user interface, but run-level batch integration, several options beyond gate-level checks, and the federated protocol and its probabilistic and budget results remain paper proofs.The proof-only scope also includes durable endorsements from aborted invocations and arbitrary mid-run matched pairs.Source: S9 Machine-Checked Verification in… · pp. 144, 146
  • Reasoning Integrity uses a lockstep simulation that equates the Protected LLM’s observations and transcript while allowing untrusted stores and hidden handle resolutions to differ.Equal transcripts also force equal sink logs, operation sequences, reply streams, and final views.Source: S9 Machine-Checked Verification in… · p. 144
  • Eight computational scenarios test interface behaviors including blocked injection, endorsement reuse, noninterference, and attack-surface confinement.The scenarios are build-time assertions; theorems are kernel-checked, while #guard scenarios additionally trust Lean’s evaluator.Source: S9 Machine-Checked Verification in… · pp. 144–145, Table S5 · p. 145
  • The top-level theorems depend only on propext and Quot.sound, with no sorryAx, but the model’s correspondence to paper semantics is not machine-checked.The paper argues for that correspondence through Table S5 and documented modeling deltas.Source: S9 Machine-Checked Verification in… · p. 145, Table S5 · p. 145

Related papers

Loading 2610.28987v1…