L3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agents

Evidence record

Primary engineering study of a Lean 4 harness with scoped capability tokens, Git-backed agent state, reversibility tiers and partial kernel-checked invariants.

Read the original source ↗

Claim-level citations (5)

• supportsL3M tests capability-bounded self-extending agents: The paper explicitly identifies conditions outside some kernel proofs, including token non-forgeability enforced by the build rather than proved by the kernel.

  Table 1, No token without the grant, Rests on column

• supportsL3M tests capability-bounded self-extending agents: L3M 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.

  Section 5.1, Staged builds: write, gate, execute

• supportsL3M tests capability-bounded self-extending agents: In the authors' Terminal-Bench evaluation, safe-only tools reached roughly two thirds of the pass rate of an unrestricted shell baseline.

  Abstract and Introduction, evaluation statement

• supportsL3M tests capability-bounded self-extending agents: The 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.

  Section 3.1, What is not claimed; Table 1, theorem assumptions and coverage

• supportsL3M tests capability-bounded self-extending agents: The 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.

  Introduction, sections 3.1–3.4; Table 1, monotone authority and sealed program guarantees