Agenra 论文提出通过形式化模拟验证 LLM Agent 权限修订以保全工作流

该论文针对 LLM Agent 部署中权限修订导致合法工作流中断的问题，提出了 Agenra，一种带有 Lean 执行核心的策略语言。其核心机制是追踪每次调用的资源消耗、运行时发现的资源以及早期调用已消耗的权限，将安全性与工作流保留视为独立属性，并通过旧与新权限账本之间的模拟来认证修订的有效性。

在 51 个作者编写的修订案例中，该检查方法成功认证了所有 21 个能够保留客户端的修订，并排除了全部 30 个无法保留的修订，且每个丢失的工作流都通过重放得到确认。此外，该方法还认证了一个开源 Agent 应用中的真实配额增加场景。值得注意的是，在一个报告交付应用中，提高发送配额虽然保留了所有客户端并允许第二次批准发送，但这证明了工作流保留并不等同于安全性。

事实层面，该研究基于序列化调用和相同服务结果的假设，信任 Python 翻译层，覆盖了未发现资源、未枚举负载、失败调用及批准情况。推断层面，这种形式化验证方法可能解决当前 Agent 权限管理中“宽泛授权即破坏流程”的痛点，但实际效果依赖于部署环境的序列化约束。猜测层面，该方法能否扩展到非序列化并发环境或处理更复杂的动态服务结果尚需进一步验证。