# OpenShell 团队用数学证明来管 AI 代理的权限，思路来自 AWS 的老经验

> 原标题：What we have learned at OpenShell applying formal methods to control AI agents

- 来源：Hacker News 首页
- 发布时间：2026-09-15T14:40:05.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/56732
- 原文：https://nvidia.github.io/OpenShell-Research/dev-notes/posts/2026-09-10-learning-formal-methods-agent-policy-prover/

## 摘要

NVIDIA 的 OpenShell 团队把安全策略写成逻辑公式，再用 Z3 这类自动求解器去算一个代理能做的操作会不会越权。他们之前在 AWS 就用同样的方法验证过 EC2、IAM 和 S3 的权限配置，现在把这套思路搬到 AI 代理的工作流里。文章一步步演示了怎么把完整的 OpenShell 策略编码成形式化逻辑，然后跑一个“包含性查询”来检查有没...

## 推荐理由

NVIDIA OpenShell 团队把形式化方法用到 AI 代理权限控制上，用 Z3 自动验证代理会不会越权——方法具体，有 AWS 生产环境验证过的底子。H 和 K 都站得住，但受众偏安全工程方向，R 上不去，正好落在 featured 档。

## 锐评

OpenShell 团队做了一件思路很直的事：把 AI 代理能做的操作和安全策略都写成逻辑公式，扔给 Z3 这类自动求解器去算，看代理会不会越权。他们之前在 AWS 就用同样的方法验证过 EC2、IAM 和 S3 的权限配置，现在把这套思路搬到代理工作流里。文章一步步演示了怎么把完整的 OpenShell 策略编码成形式化逻辑，然后跑一个“包含性查询”来检查有没有缺口。

但全文没有给出任何性能数字，也没提生产环境下的误报率。这意味着我们不知道这套方法在代理规模变大时会不会算不动，也不知道它会不会把正常操作误判成违规。文章自己也定位成工程笔记，讲的是可行性和方法，不是成熟方案。

还缺两样东西：一是这套证明在代理实际运行时的延迟和资源开销，二是它跟现有基于规则或 LLM 判别的权限控制相比，到底能多拦住多少真实攻击。没有这些，就只能说方向对，但离落地还有距离。