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

What we have learned at OpenShell applying formal methods to control AI agents

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

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