L3M separates state, instructions and authority. Its Git-backed trajectories can be resumed and compared, while tools require explicit capability tokens and child grants cannot exceed their parent under the modeled rule. Reversibility determines which effects require review. The authors emphasize that kernel-proved invariants sit alongside trusted…
Inspect the ClaimsCase · DiggingBeagle record
L3M tests capability-bounded self-extending agents
L3M makes an agent-created Lean program request typed capabilities rather than inheriting unrestricted shell authority, with an explicit performance trade-off.
Scope
Prototype runtime and authors' evaluation, not independent certification of an agent sandbox, deployed containment, or general-purpose proof of absence of prompt injection.
Assessment profile
Assessment method- Setting
- research demonstration
- Exploitation
- not established
- Evidence
- Grade B
- Remediation
- not applicable
- AI role
- AGAINST AI
Basis and provenance
Direct reading of the authors' technical paper confirms a prototype with selected kernel-checked invariants, explicit trusted-base assumptions and a Terminal-Bench utility measurement. It is not a demonstrated exploit, certified deployed sandbox or comprehensive proof of safety.
Assessed Oct 16, 2026 using diggingbeagle.assessment/1.
Evidence basis: CLM-L3M-LIMIT · CLM-L3M-UTILITY · CLM-L3M-CAPABILITY · CLM-L3M-BOUNDARIES · CLM-L3M-STAGED · L3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agents
At a glance
The important comparison is actual side-effect authority, not whether the LLM describes itself as safe. The design also exposes the cost of reducing implicit capabilities.
Read the implicationsThe safety guarantees cover the implementation and assumptions identified by the paper; they are not a universal security guarantee. Agent performance, review burden and practical operator usability require further independent evaluation. The authors state that their theorems cover individual runtime checks, not a global safety guarantee, and do not prove…
Limits and uncertaintyFull account
L3M separates state, instructions and authority. Its Git-backed trajectories can be resumed and compared, while tools require explicit capability tokens and child grants cannot exceed their parent under the modeled rule. Reversibility determines which effects require review. The authors emphasize that kernel-proved invariants sit alongside trusted assumptions about token construction, filesystems and providers. An untuned safe-only setup performed below an unrestricted shell baseline. The central security distinction is between a capability an agent can use and permission to enlarge that capability. A sealed self-authored Lean program may reuse only effect classes and tokens permitted by the initial grant; a child grant is checked against the parent at spawn. The proposed staged-build workflow separates writing source, approving its exact bytes and executing them, while networking and access to private data are assigned to different roles. These patterns narrow available effects, but the authors explicitly do not claim a session-wide proof. A bad initial grant, an unsafe external provider, an unsandboxed shell or untrusted Lean elaboration can remain outside specific theorems.
Mechanism and trust boundary
- 01
Human grants capabilities
File roots, network access and budgets are represented by scoped grants.
Boundary: human approval to agent runtime
- 02
Agent proposes a new program
Lean types name required capabilities and the seal mechanism limits admitted constants.
Boundary: model-generated code to runnable tool
- 03
Runtime executes controlled effects
An effect takes a token, and irreversible or unbounded effects enter review.
Boundary: approved capability to operating-system effect
Timeline
- Oct 14, 2026disclosure
Public disclosure
Claims & evidence
CLM-L3M-LIMITThe paper explicitly identifies conditions outside some kernel proofs, including token non-forgeability enforced by the build rather than proved by the kernel.supported
Basis: reported finding
- supportsL3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agentsprimary disclosure
Table 1, No token without the grant, Rests on column
CLM-L3M-STAGEDL3M describes a staged build workflow that separates a writer, a byte-hash approval gate and a runner; its authors caution that compilation can execute code and still needs independent sandboxing.supported
Basis: reported finding
- supportsL3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agentsprimary disclosure
Section 5.1, Staged builds: write, gate, execute
CLM-L3M-UTILITYIn the authors' Terminal-Bench evaluation, safe-only tools reached roughly two thirds of the pass rate of an unrestricted shell baseline.supported
Basis: reported finding
- supportsL3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agentsprimary disclosure
Abstract and Introduction, evaluation statement
CLM-L3M-BOUNDARIESThe paper explicitly states that it has no session-wide safety theorem, that whole-runtime composition is argued rather than proven, and that an unsandboxed shell is outside its confinement argument.supported
Basis: reported finding
- supportsL3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agentsprimary disclosure
Section 3.1, What is not claimed; Table 1, theorem assumptions and coverage
CLM-L3M-CAPABILITYThe L3M paper describes a Lean 4 runtime in which sealed self-authored programs use admitted capability tokens, and child authority is checked against parent grants.supported
Basis: reported finding
- supportsL3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agentsprimary disclosure
Introduction, sections 3.1–3.4; Table 1, monotone authority and sealed program guarantees
Implications
The important comparison is actual side-effect authority, not whether the LLM describes itself as safe. The design also exposes the cost of reducing implicit capabilities.
Controls and mitigations
- Grant file, Git, process and network authority through narrow runtime capabilities and enforce those checks at effect execution, rather than relying on a model to self-police. This is an architectural principle illustrated by L3M, not proof that any other harness implements it.
- Split modification of executable bytes from their approval and execution. Pin reviewed bytes by digest and run them under separate sandboxed authority where practical. The paper warns that compilation and elaboration themselves may execute code.
- Treat token non-forgeability, filesystem symlink handling, providers, and the initial human grant as part of the trusted base when evaluating the prototype.
Unknowns and contradictions
- The safety guarantees cover the implementation and assumptions identified by the paper; they are not a universal security guarantee.
- Agent performance, review burden and practical operator usability require further independent evaluation.
- The authors state that their theorems cover individual runtime checks, not a global safety guarantee, and do not prove malicious Lean source harmless during load.
- Preventing exfiltration additionally depends on how a human separates read and network grants. Capabilities cannot infer that an authorized data transfer is inappropriate.
Sources and citation
Material revision history
- Oct 16, 2026 · Canonical change recorded · new in release · revision 157