能力可以涨，权限不能涨

能力可以涨，权限不能涨

Agent 干长活时最大的瓶颈，往往不是模型不够聪明，而是人不够用。一项横跨几天、多个 agent、大量工具调用的计算里，有三类参与者：人决定什么重要、模型处理模糊、代码负责计算和等待——三个人里，只有人的注意力不会随需求扩展。亚马逊一个五人团队把这层观察写成了一个运行时的设计前提：计算要长大，前提是人不在每个环里。这就是 L3M（Lean + Large Language Models，arXiv 2610.19591，v1 于 10 月 14 日挂出）——整个 harness 用 Lean 4 写成，同一种语言负责三件事：实现系统、声明不变量、充当 agent 扩展系统的语言。

第一个机制解决「agent 自己长工具」的安全问题。agent 在工作中琢磨出一个可复用的流程，可以把它写成一段密封的 Lean 程序——程序的类型就是它的权限申请单，harness 按类型收缴执行。运行时启动时按授权铸造能力令牌：允许写哪些目录、能碰哪些 Git 分支前缀、能访问哪些网络，每个要触碰文件系统、进程、网络或模型的操作都必须出示对应令牌。于是有了一句铁律，论文原文只有五个词：Capability grows; authority does not——能力可以涨，权限不能涨。多智能体场景下权限沿委派树只减不增；职责分离做成了 W^X：能提出危险调用的模型没有批准权，批准它的另一个模型手里没有任何工具，两条职责绑不成一条攻击链。

第二个机制是 Git 当时光机。工作产物、往来邮件、权限凭证、生命周期，全部是共享仓库里的 ref；恢复、回滚、分叉、对比、合并都是运行时原语——两个 agent 可以在两条分支上试不同的路，输了的那条连同历史一起归档。等待、通信、委派、撤销，这些原本要模型自己现想模式的事，变成了运行时的基础设施。

第三个机制决定人什么时候需要出场：按可逆性分级。审阅级别从工具的足迹推导——运行时能撤销的动作（读文件、带日志的编辑、本地提交）属于「温驯」，agent 直接做不必请示；影响无法收回的动作才升级审阅，初审默认用小模型，被驳回后提交方可以补充理由进二审，谈不拢的死结才落到人类的审阅卡上。实测里被审的调用最终约九成判安全，约 6% 被重定向到免审的等价工具（想跑 grep 就改用文件工具的 grep），2% 撤回，真正的死结占 2.4%。

这篇报告最有分量的部分是它对「可信」的诚实边界。核心保证表里每一条都是一个 Lean 定理：文件工具无法命名一个爬出授权根目录的路径、子代理权限必然窄于父级——改坏已证属性的代码直接编译不过。但论文随即自己泼冷水：不存在会话级的安全定理，定理只说明一次工具调用能做什么，不说明该不该做——「一个出于坏理由做出的温驯动作，依然是温驯的」，而且任何定理都不担保补丁本身正确。代价也标了价：Terminal-Bench 37 个任务上，Claude Code 跳过权限跑出 59.5% 的通过率，L3M 同配置关掉审阅只有 41.7%——这 18 个百分点就是权限绑定的价格；只用免审工具的纯温驯档掉到 27%；每次审阅平均多花 2.6 次模型调用、中位 8.6 秒。

此前的 Sandcastle 系统里有一条判断：审批能不能省，取决于动作搞砸了有多难收拾。L3M 把这条朴素判断做成了整个系统的地基——难收拾的程度就是可逆性，而且不是口头承诺，是要在类型系统里给出「撤销后精确还原」的证明才算数。更难得的是这篇论文没有回避代价，而是把价格签直接挂了出来：安全不是免费的，18 个百分点、每次审阅 8.6 秒、2.4% 的人类介入率，就是让计算在没有人盯着的情况下长大的成本。