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

Summary

PerMIT is a memory architecture for LLM agents that gives provable integrity guarantees under an explicit trust assumption: only user-typed inputs and values confirmed at a gate are trusted. Two integrity theorems, machine-checked in Lean 4, ensure environment-derived memory reaches a sensitive action only if confirmed at the gate. On Trojan Hippo, PerMIT records zero observed attack success, and on τ²-bench, communities of up to 90 autonomous agents build shared knowledge bases with no direct memory injection promoted.

Related items

• InfoIs Claude Code safe for the enterprise? What the official settings cover, and what they don'tSimilar attack · Adversa AI Blog
• Info‘Context Bombs’ Cut AI Attack Success by Misleading Agents With Fake TargetsSimilar attack · SecurityWeek
• InfoPrompt Injection Through Forensic Evidence: A Taxonomy and Proof of Concept of Anti-Forensic Attacks on LLM-Assisted Digital InvestigationsSimilar attack · Arxiv (cs.CR + cs.CL + cs.LG)
• InfoThe Harness Is the Hard Part of Agentic PentestingSimilar attack · The Hacker News
• InfoWhere AI Vulnerability Discovery Harnesses Go Quiet: Structural False Negatives and Hidden VulnerabilitiesSimilar attack · Arxiv (cs.CR + cs.CL + cs.LG)