Capability Grows, Authority Does Not: L3M, a Lean 4 Runtime for Long-Running Agents
When agents run long jobs, the biggest bottleneck is often not model intelligence but human availability. In a computation spanning days, multiple agents, and thousands of tool calls, there are three kinds of participants: humans decide what matters, models handle ambiguity, and code does the computing and waiting. Of the three, only human attention does not scale with demand. A five-person Amazon team turned this observation into a runtime design premise: computation should be allowed to grow on the assumption that no human is in every loop.
That premise became L3M (Lean + Large Language Models, arXiv 2610.19591, v1 posted October 14). The entire harness is written in Lean 4, and the same language serves three roles: implementing the system, declaring invariants, and serving as the language agents use to extend the system.
Mechanism 1: Agents grow their own tools, safely
When an agent discovers a reusable workflow, it can write it as a sealed Lean program. The program's type is its permission request; the harness collects and executes it according to type. At startup, the runtime mints capability tokens based on authorization: which directories may be written, which Git branch prefixes can be touched, which networks are reachable. Every operation touching the filesystem, processes, network, or models must present the corresponding token.
Hence the iron rule—five words in the original paper: Capability grows; authority does not.
In multi-agent settings, permissions along the delegation tree only narrow. Separation of duties is enforced as W^X: a model that can propose a dangerous call has no approval power, and the model that approves it holds no tools at all—two responsibilities that cannot be chained into a single attack path.
Mechanism 2: Git as a time machine
Work products, exchanged messages, permission credentials, and lifecycles are all refs in a shared repository. Restore, rollback, fork, diff, and merge are runtime primitives—two agents can try different paths on two branches, and the losing branch, along with its history, is archived. Waiting, communication, delegation, and revocation—patterns models previously had to improvise—become runtime infrastructure.
Mechanism 3: Human review triggered by irreversibility
Review levels are derived from a tool's footprint. Actions the runtime can undo (reading files, logged edits, local commits) are "docile" and proceed without asking. Only irreversible actions escalate review: a small model performs first review, the submitter can add justifications for a second review after rejection, and only genuine deadlocks land on a human review card.
In practice, roughly 90% of reviewed calls were ultimately judged safe, ~6% were redirected to review-free equivalent tools (want to run grep? use the file tool's grep), 2% were withdrawn, and true deadlocks accounted for 2.4%.
Honest limits of "trustworthiness"
The most weighty part of the report is its candor about trust. Every entry in the core guarantee table is a Lean theorem: the file tool cannot name a path escaping the authorized root; sub-agent permissions are necessarily narrower than the parent's—code that breaks a proven property simply fails to compile.
But the paper immediately pours cold water on itself: there is no session-level safety theorem. Theorems only state what a single tool call *can* do, not whether it *should* be done—"a docile action taken for bad reasons is still docile"—and no theorem guarantees that a patch itself is correct.
The price tag
On 37 Terminal-Bench tasks, Claude Code without permission enforcement scored 59.5% pass rate; L3M in the same configuration with review disabled scored only 41.7%—those 18 percentage points are the price of capability binding. Using only review-free (purely docile) tools dropped performance to 27%. Each review costs on average 2.6 additional model calls and a median of 8.6 seconds.
An earlier system, Sandcastle, had a judgment: whether approval can be skipped depends on how hard a botched action is to clean up. L3M turned that plain judgment into the foundation of the whole system—difficulty of cleanup *is* reversibility, and it is not a verbal promise; it requires a type-level proof of exact restoration after undo.
What is most commendable is that the paper does not dodge the cost—it hangs the price tag openly: safety is not free. 18 percentage points, 8.6 seconds per review, and a 2.4% human intervention rate are simply the cost of letting computation grow without anyone watching.