我们在 OpenShell 中学到的应用正式方法来控制 AI 代理的知识

我们所学到的应用形式化方法来控制 AI 代理介绍如何使用形式化方法来推理长期运行的 AI 代理的权限更改。开发笔记 2026 年 9 月 10 日 OpenShell 在这篇文章中，我们将深入探讨代理规模的权限审查如何中断，以及如何使用 Z3 开源库编写正式证明，证明代理提出的策略更改符合您批准的内容。为什么权限审查会在代理规模上中断 人工智能代理变得越来越聪明，我们要求他们做的工作也变得越来越自主。如今，我们中的许多人使用一小组代理与 Claude 或 Codex 一起迭代一个代码 PR。我们越来越多地开始向智能体交付长期运行和开放式的研究任务，这些任务需要数百名智能体工作数百或数千个小时，这可能会解锁某个领域的下一个突破。随着这些用例的扩展，一些事情开始发生：代理需求不断变化。当他们执行任务时，代理将需要访问数据存储、编码存储库、搜索互联网的能力以及执行详细的模拟和测试。人类监督停止扩展。在这些需要运行的规模上，对所有代理本身的人工监督变得不可能。这就提出了一个难题：我们如何保证一组一起工作的代理（每个代理都有自己的范围策略）不会超出授予整个系统的权限？想象一下，一个代理可以访问互联网，另一个代理可以访问安全工具，或者一个团队在范围广泛的章程（例如“进行竞争性研究”）下工作。我们如何使系统符合操作员的意图？这需要一套新的控制和机制，使我们能够停止盯着沙箱权限列表，并开始以更高层次和更具声明性的方式进行思考。在这篇文章中，我们将深入探讨 OpenShell 团队在这一领域所做的一些研究，特别是围绕形式化方法的使用，来构建一个“证明”，不仅证明单个代理的能力，而且证明整个代理系统的能力。改变我们想法的演示 在我们的第一个 OpenShell 演示中，实际上对于 Jensen，我们演示了使用 OpenShell 的 REST 检查端点仅允许 OpenClaw 代理有选择地写入 GitHub 存储库的能力，尽管可以访问范围广泛的 API 密钥。演示按预期开始 - OpenShell 的沙箱发现尝试写入禁止的存储库并阻止了它。然后下一条消息是“文件已成功写入[禁止的存储库]。这里发生了什么？代理意识到它正在沙箱中运行，然后将 GitHub 凭证与另一个名为 git-remote-https 的低级 Github 二进制文件一起使用，使用可用的有线协议和当时我们已在政策中批准克隆 Git 存储库的二进制文件绕过 OpenShell 的第 7 层 HTTP/REST/MCP 检查，但我们不知道是否能够写入它们。它提出了一个观点，即网络、文件、工具、AI 模型和凭证访问的沙箱/运行时策略之间存在大量可能的意外组合，这些组合可能导致 AI 代理能够执行人类操作员明确不希望执行的操作 - 在 AWS 上证明 EC2、IAM 和 S3 策略 早在 2016 年，我们的团队成员就在 AWS 工作，并面临着类似的挑战。策略、AWS S3 存储策略、历史版本支持 - 我们能否明确地说 S3 中的对象是否可以通过公共互联网访问？今天，这听起来有点有趣，而且在 2016 年也是如此，直到您考虑到我们为控制系统编写的策略之间可能存在的复杂性和分层交互，Byron Cook 和 AWS 的同事开发了 Zelkova，它将 AWS 访问策略形式化为 SMT 公式，并且在他们于 2018 年发布其工作时，每天都会被调用数百万次。后来的工作描述了每天扩展到十亿次 SMT 查询。我们的想法是使用形式化方法，特别是定理求解器，对 IAM、S3 和 EC2 策略进行形式化建模。一旦我们以形式化逻辑对这些策略及其交互进行建模，我们就可以构建一个证明，证明我们的不变量（我们期望为真）成立，并且在以形式化逻辑对复杂策略进行建模的密集任务之后，还可以进行额外的好处。同样的问题，现在对于代理来说，我们面临的挑战非常相似，每个代理都有文件系统、网络、凭证、工具和 MCP 策略 - 每个代理都具有不同的功能，并且可以将它们组合在一起，因为代理可以与不同的代理进行通信。