Persistent memory is a largely undefended surface for injection and poisoning, limiting memory sharing among agents. We introduce PerMIT, a memory architecture that offers 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 selection. Over this interface we formalize and machine‑check in Lean 4 two integrity theorems that ensure environment‑derived memory can reach a sensitive action only after gate confirmation and can influence the agent only via what the gate displays. Consequently every attack in our threat model reduces to a single auditable decision that a human, an LLM verifier, or both can make. In the Trojan Hippo scenario PerMIT records zero successful attacks when combined with self‑verification and lightweight verifiers. Because each confirmation logs an exact verdict, endorsements accumulate across users; sufficiently endorsed items become community‑confirmed without further verification. Under the explicit assumptions we prove and corroborate in simulation a co‑scaling property: as the community grows, the risk of promoting poison and of wrongly evicting benign knowledge both drop, while per‑user verification effort does not increase. On the $\\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.
Review