L3M: A Verifiable Harness and Runtime for Self-Extending and Self-Improving Agents
L3M asks how to run AI agents so that useful computation scales safely across days, machines, and model calls. It answers with a Git-backed, distributed runtime written in Lean 4 where capability tokens confine every tool call, trajectories are durable append-only logs, and agents self-extend by writing sealed programs whose types bound their authority. The goal is a harness where trust narrows rather than widens as agents grow more capable.
The paper presents a mature, opinionated architecture that treats agent harness design as a security and systems problem rather than an API problem. Its capability-token model and reversible-action design are intellectually coherent and distinct from dominant loop-based harnesses. However, the empirical evaluation is thin: on 37 Terminal-Bench tasks L3M trails Claude Code by a wide margin (27% vs 59.5% pass@3 with only tame tools), and the benefits of self-extension and tool programs remain marginal. The authors are admirably careful in delineating what is proved versus what is trusted, yet several key guarantees are explicitly "argued by construction and pinned by tests, not proved," leaving a meaningful gap between the formal story and the runnable system.
The runtime architecture is the standout contribution. Anchoring all agent state in Git refs, making trajectories pure folds over an append-only Log, and encoding authority as monotonic refineable grants creates a principled foundation for long-lived multi-agent systems. The separation-of-duties patterns — staged builds, quarantined readers, private and public agent splits — show how formal security concepts can yield practical engineering benefits. The design choice to keep reasoning in the model while loops and state operations run as code sidesteps a bottleneck inherent in model-centric loop architectures.
The empirical evaluation does not yet justify the claim that this architecture enables self-improving agents at scale. On Terminal-Bench, L3M with all tame tools achieves only 27% pass@3 against Claude Code's 59.5%, and adding shell access with review still leaves a large gap. Self-extension via sealed programs adds a mere 2.7 percentage points in the tame setting, and token costs for passing attempts are roughly 75% higher than Claude Code's (7.7M vs 4.43M), suggesting significant overhead. More fundamentally, several formal claims are explicitly scoped down: there is no session-wide safety theorem, and the confinement of malicious Lean source during elaboration is "argued by construction and pinned by tests, not proved." The trusted base is also substantial — it includes the Lean kernel, Linux kernel, model provider API, and several external binaries — which limits how much the proved theorems reduce operational attack surface.
The comparison to Claude Code is fair as a point-in-time cost-of-security measurement, but the benchmark is small (37 tasks selected for a median runtime under one hour) and the L3M implementation is explicitly untuned. The paper does not compare against other agent frameworks that offer sandboxing or approval workflows, which leaves open how much of the gap is inherent to capability discipline versus implementation immaturity. The authors correctly separate the proved invariants from the empirical workload, but readers may overread the headline guarantees because the surrounding discussion frames them as securing "self-extending and self-improving agents" while the evaluation stays at the level of an unmodified coding benchmark.
The paper does not mention public release of code, data, or build instructions. Independent reproduction would require the Lean-based runtime, hub daemon, provider integrations, and the exact grant and persona configurations used for Terminal-Bench. The hyperparameters (model versions, token limits, review prompts, reviewer model choice) are documented, but without the toolchain itself the experiment is not reproducible. Because the guarantees rest on Lean proofs, reproducing the formal claims additionally requires building the project and checking the theorems, yet no repository or artifact link is provided.
The lasting gains in AI have come from methods that absorb more computation, and language models already scale computation within a call. Useful work, though, happens across calls: over hours or days, through tools and external systems, among many agents and the humans they work for, and increasingly through code the agents write themselves. Whether that work compounds is enabled by the harness around it, and the harness faces a constraint the model does not: of the three participants in such a computation, the human, the model and code, only the human's attention does not scale, so the computation can grow only if the human is not in every loop. L3M is a runtime built on that premise, written in Lean 4 so that one language implements the harness, states its invariants, and is the language agents extend it in. One computation spans humans, agents, models and code, and all of its state lives in Git: a rich state trajectory -- rather than a chat conversation -- is an object the runtime can resume, rewind, fork, compare and merge. Waiting, communication, delegation and undo are primitives, not patterns the model reasons through each time. When an agent works out a procedure, it can write it once as a sealed Lean program whose type is its permission request, and the harness offers it back as a tool -- machinery for the model to use. To take the human out of the loop, L3M uses reversibility to decide where that is safe: a tool's review tier follows from how far its effects can be undone, so agents act freely where the runtime can recover. Because the machinery can change, the properties that make this safe are stated as kernel-checked theorems about the code that runs. On Terminal-Bench, an untuned L3M reaches about two thirds of its (unsafe) shell-equipped pass rate using only safe (not needing human review) tools.
Pick a starting point or write your own. Challenges run in the background, so you can keep reading while the AI investigates.
No challenges yet. Disagree with the review? Ask the AI to revisit a specific claim.