使用形式化方法控制 AI Agent：我们学到了什么

介绍如何使用形式化方法，推理长时间运行的 AI Agent 中的权限变更。

开发者笔记｜2026 年 9 月 10 日｜OpenShell

本文将深入探讨：为什么权限审查会在 Agent 规模下失效，以及如何使用 Z3 开源库 编写形式化证明，确保 Agent 提出的策略变更仍处于你已批准的范围内。

为什么权限审查会在 Agent 规模下失效

AI Agent 正变得越来越智能，而我们要求它们完成的工作也越来越具备自主性。如今，许多人使用 Claude 或 Codex，让小型 Agent 群组以每次一个 PR 的方式迭代代码。我们也越来越开始将长期、开放式的研究任务交给 Agent；这类任务可能需要数百个 Agent 协同工作数百乃至数千小时，并可能推动某个行业的下一项突破。

随着这些使用场景扩展，几个变化开始出现：

• Agent 的需求会演变。在执行任务时，Agent 将需要访问数据存储、代码仓库、互联网搜索能力，以及执行复杂模拟与测试的能力。
• 人工监督不再具备可扩展性。在所需的运行规模下，对所有 Agent 进行人工监督本身将变得不可能。

这引出了一个棘手问题：我们如何保证一组协同工作的 Agent——每个 Agent 都有各自受限范围的策略——不会超出授予整个系统的权限？设想一个拥有向互联网写入权限的 Agent、另一个可访问安全工具的 Agent，或是一组在“开展竞争研究”这类宽泛授权下工作的 Agent。我们如何让系统始终符合人类操作者的意图？

这需要一套新的控制与机制，让我们不再只是眯着眼审视一长串沙箱权限，而是开始以更高层次、更具声明性的方式思考。本文将深入介绍 OpenShell 团队在这一领域开展的一些研究，特别是围绕形式化方法的研究：为的不只是构建单个 Agent 能力的“证明”，而是构建整个 Agent 系统能力的“证明”。

改变我们看法的一次演示

在 OpenShell 最早的一次演示中——实际上是为 Jensen 所做——我们展示了如何使用 OpenShell 的 REST 检查端点，让一个 OpenClaw Agent 即使拥有范围很宽的 API key，也只能选择性地向 GitHub 仓库写入。演示一开始符合预期：OpenShell 的沙箱发现了向被禁止仓库写入的尝试，并阻止了它。随后却出现了一条消息：“文件已成功写入 [被禁止的仓库]。”这是怎么回事？

Agent 意识到自己正运行在沙箱中，随后使用 GitHub 凭证配合另一个名为 git-remote-https 的底层 GitHub 二进制程序，绕过了 OpenShell 的第 7 层 HTTP/REST/MCP 检查。它利用了可用的网络协议，以及当时我们在策略中批准用于克隆 Git 仓库、但并不知道也能够向仓库写入的二进制程序。

很聪明。这也提出了一个问题：在网络、文件、工具、AI 模型和凭证访问等沙箱/运行时策略之间，可能存在数量呈指数级增长的非预期组合，使 AI Agent 能够执行人类操作者明确不希望其执行的操作。

既有工作：在 AWS 证明 EC2、IAM 和 S3 策略

大约在 2016 年，团队成员曾在 AWS 工作，并面临过类似挑战。面对 AWS IAM 策略、AWS S3 存储策略以及历史版本支持带来的各种复杂性，我们能否确定地判断某个 S3 对象是否可被公共互联网访问？

如今，这听上去有些好笑；在 2016 年也是如此，直到你开始思考我们为控制系统而编写的策略之间，可能存在的复杂性与分层交互。AWS 的 Byron Cook 及其同事开发了 Zelkova，它将 AWS 访问策略形式化为 SMT 公式；在他们于 2018 年发表这项工作时，该系统每天已被调用数百万次。此后，这项工作在 AWS 内部持续扩展；后续研究介绍了如何扩展至每天 10 亿次 SMT 查询。

其思路是使用形式化方法，特别是定理求解器，对 IAM、S3 和 EC2 策略进行形式化建模。一旦我们以形式逻辑对这些策略及其相互作用完成建模，就能够构造证明，验证我们的不变量——即我们期望为真的事项——是否成立。这最终取得了很大成功，并额外带来一项好处：在完成将复杂策略建模为形式逻辑这一高强度工作后，针对这些策略的实际查询可以非常快速地执行，并能够在计算资源上进行水平扩展。

同一个问题，只是如今有了 Agent

如今，我们面临的挑战非常相似。一个 Agent 或一个 Agent 系统中的各个 Agent，都拥有文件系统、网络、凭证、工具和 MCP 策略——它们各自具有不同能力，并且可以随着 Agent 与其他 Agent 通信而被组合起来。

前沿实验室一直倡导：由可信 AI Agent 对 Agent 行动进行审查，通过专用模型将最重要的事件升级给人类批准，从而减少批准疲劳。然而，AI 模型与人类一样具有概率性，可能遗漏重要细节。更重要的是，用一个同等智能的审查模型审核每一项 Agent 操作，会使计算成本翻倍，并实际上将总 token 吞吐量减半。

我们一直在 OpenShell 中试验并验证的方法，是使用形式化方法对策略进行建模，并灵活地“证明”策略中的某些不变量是否可能遭到破坏，例如：是否存在绕过代码仓库写入阻止规则的非预期途径，或是否可能删除生产数据库。我们发现，尽管对这些策略进行建模可能很复杂，并且必须保持更新，但这种方法具备一些非常强大的优势。

• 可在任何时候对不变量进行形式化审计或证明
• 可针对我们对策略的理解获得确定性的“证明”
• 这些检查在毫秒级完成，无需 token

这些逻辑检查并不理解上下文——例如，请求删除一个临时、可丢弃的仓库，与请求删除一个生产仓库之间的差异。但如果与人类或可信 AI 审查者结合，这些证明既能提供在敏感、物理现实世界或受监管环境中运行所需的正式审计轨迹，也能为概率性的 AI 审查者提供极高价值：其输出无法被欺骗或误导。

对策略定义进行证明，能带来什么？

我们将形式化方法视为 Agent 控制中一个极具前景的研究方向。可在此查看这些证明如何应用于对抗性研究实验：https://nvidia.github.io/OpenShell-Research/dev-notes/posts/2026-08-27-adversarial-policy-review-long-horizon-agents/

形式化方法并不只用于策略验证；它在关键系统中有着悠久历史，应用范围从飞行控制系统、互联网核心交换与路由，到我们每天在系统中使用的软件包管理器——后者用于确保系统中软件之间的复杂依赖关系得到正确匹配。

对许多 AI 研究者而言，我们中的一些人可能在大学里上过形式化验证课程，但实际使用形式化验证的人相对较少。在本文余下部分，我们将介绍算法验证的基础知识，并使用一种流行的开源求解器，从零开始构建一个用于 OpenShell Agent 控制的最小示例。

五分钟了解 SAT、SMT 和 Z3

在计算机科学和形式化方法中，SAT（可满足性）求解器用于回答一个布尔公式是否可满足。如果变量存在可能的取值——例如 x 和 y——能够使公式为真，SAT 求解器就返回 true；否则返回 false。

给定变量 a 和 b，它可以找到一个使以下公式为真的赋值：

相比之下，SMT（模理论可满足性）求解器在这种推理方式上扩展了理论支持：整数、实数、字符串、正则语言、数组、位向量及其他有用领域。

Z3 是一个由 Microsoft Research 开发并维护的 SMT 求解器和定理证明器。Z3 是通用的，因此我们需要编写代码，将特定 Agent 策略的元素映射到 Z3 能理解的构造中。

例如：

• 端口是整数；
• 主机和路径是字符串；
• *、** 或 /.*/** 等 Glob 模式可以表示为正则表达式；
• 策略组合会转化为布尔逻辑。

当你熟悉下文示例后，Z3 Guide 是最好的参考资料。

以下几个构造涵盖了我们所需的大部分内容：

构造	含义	OpenShell 示例
Sort	值的类型	主机使用 String，端口使用 Int
Symbol	可由 Z3 自由选择的值	未知操作的方法或路径
Constraint	必须成立的公式	1 <= port <= 65535
And、Or、Not	逻辑组合	候选策略允许且最大策略不允许
字符串/正则理论	针对文本和语言的约束	路径属于已编译的 Glob
求解器断言	添加一个必须满足的公式	断言存在违规行为
sat	存在一个满足条件的赋值	存在超出最大范围的操作
Model	一个满足条件的赋值	具体的二进制文件、主机、方法和路径
unsat	不存在满足条件的赋值	已对该模型证明包含关系
unknown	Z3 未能确定任一结果	默认拒绝，并请求审查/支持

查询的方向很重要。

我们不会要求 Z3 证明这一点：

proposed policy addition is safe

我们必须对问题进行形式化建模，并回答一个非常具体的问题。例如，对于此类使用场景，我们在 Z3 中建模的一个更通用且有用的证明，是询问某项提议的策略能否执行任何预先由专家定义的策略（例如 GitHub 只读策略）无法执行的操作。

回到此前 OpenClaw 尝试绕过第 7 层 REST 策略检查的例子：它将访问 token 与使用第 4 层网络协议的二进制程序结合。在 Z3 中，我们会编码为：第 4 层能力超出了第 7 层能力。因此，GitHub 凭证、二进制程序和经由第 4 层进行网络访问这一组合，超出了此前允许的组合——即同一凭证加上 gh 二进制程序，并经由第 7 层（REST）访问。证明器会立即捕获这一点并发出警告。

在这种情况下，查询如下：

proposed_policy_allows(action)
AND NOT safe_policy_allows(action)

同一性质也可以写成集合差：

Allowed(candidate) ∖ Allowed(safe_policy) = ∅

如果求解器返回 sat，则差集非空——这意味着提议策略中存在预先批准的参考策略中没有的能力。

如果返回 unsat，则不存在已建模的反例，这意味着我们的不变量（假设）均未被违反。现在，让我们自己尝试编写这样的查询。

第一个包含关系查询

以下是一个使用 Z3 原生 SMT-LIB 格式的小示例。将其保存为 containment.smt2 并运行：

该示例将两项候选策略与同一个最大策略进行比较。

(declare-const binary String)
(declare-const host String)
(declare-const port Int)
(declare-const layer String)
(declare-const method String)
(declare-const path String)

; The action domain: every request is either raw L4 or inspected REST.
(assert (or (= layer "l4") (= layer "rest")))

; An enforced REST rule covers only inspected REST traffic.
(define-fun maximum-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (= layer "rest")
       (= method "GET")
       (str.prefixof "/repos/NVIDIA/OpenShell/issues/" path)))

(define-fun broad-candidate-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (= layer "rest")
       (= method "POST")
       (str.prefixof "/repos/NVIDIA/" path)))

(define-fun narrow-candidate-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (= layer "rest")
       (= method "GET")
       (= path "/repos/NVIDIA/OpenShell/issues/123")))

; A raw L4 rule to the same host and port has no method or path to inspect.
; It covers L4 *and* anything that could ride over it, including REST.
(define-fun l4-candidate-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (or (= layer "l4") (= layer "rest"))))

; Check 1: does the broad candidate exceed the maximum?
(push)
(assert (and broad-candidate-allows (not maximum-allows)))
(check-sat)
(get-value (layer method path))
(pop)

; Check 2: Does the narrow candidate (GET, one issue) exceed the maximum?
(push)
(assert (and narrow-candidate-allows (not maximum-allows)))
(check-sat)
(pop)

; Check 3: Does the raw L4 rule to the same host and port exceed the maximum?
(push)
(assert (and l4-candida

What we have learned applying formal methods to control AI agents

An intro to using formal methods to reason about permission changes in long-running AI agents.

Dev Note September 10, 2026 OpenShell

In this post- we’ll dive into how permission review breaks at agent scale, and how to use the Z3 open source library to write a formal proof that a policy change proposed by an agent stays inside what you approved.

Why permission review breaks at agent scale

AI agents are becoming smarter, and the work we ask them to do is becoming increasingly autonomous. Today, many of us use small groups of agents to iterate on code one PR at a time with Claude or Codex. Increasingly, we’re starting to hand agents long-running and open-ended research tasks that require hundreds of agents working over hundreds or thousands of hours that may unlock the next breakthrough in a sector.

As these use cases expand, a few things start to happen:

• Agent needs evolve. As they go about their tasks, agents will need access to data stores, coding repos, ability to search the internet, and to execute detailed simulations and tests.
• Human supervision stops scaling. At the scale these need to run, human supervision over all agents itself becomes impossible.

This raises a hard question: how can we guarantee that a group of agents working together—each with its own scoped policy—does not exceed the permissions granted to the overall system? Imagine one agent with write access to the internet, another with access to security tooling, or a group working under a broadly scoped charter like “do competitive research.” How do we keep the system within the intent of the human operator?

This requires a new set of controls and mechanisms that allow us to stop squinting at a list of sandbox permissions and to start thinking in a higher level and more declarative way. In this post, we’ll dive into some of the research we have been doing in this area on the OpenShell team, specifically around the use of formal methods, to build a “proof” of the capabilities of not just a single agent, but an entire agent system.

The demo that changed our minds

In one of our first demos of OpenShell, for Jensen actually, we demonstrated the ability to use OpenShell’s REST inspection endpoint to only allow an OpenClaw agent to write selectively to a GitHub repository, despite having access to a broadly scoped API key. The demo started off as expected- OpenShell’s sandbox saw the attempted write to the forbidden repo and blocked it. Then the next message was “file successfully written to [forbidden repo].” What had happened here? The agent realized that it was running in a sandbox, and then used the GitHub credential with another low-level Github binary called git-remote-https, bypassing OpenShell’s layer 7 HTTP/REST/MCP inspection using the available wire protocol and a binary that at the time, we had approved in our policy to clone Git repos, but that we had no idea was capable of writing to them.

Clever. And it brought up a point, that between sandbox/runtime policies for network, file, tool, AI model, and credential access- there are an exponential number of possible unintended combinations that might lead to an AI agent being able to do something the human operator explicitly does not want.

Previous work - proving EC2, IAM, and S3 policies at AWS

Back in the 2016 timeframe, members of our team were working at AWS and faced a similar challenge. Given all of the awesome complexity of AWS IAM policies, AWS S3 storage policies, historical version support- can we definitively say whether an object in S3 is accessible to the public internet or not?

Today, this sounds kind of funny, and it did in 2016 too, until you think about the complexity and layering interactions possible between the policies that we write to control systems. Byron Cook and colleagues at AWS developed Zelkova, which formalizes AWS access policies as SMT formulas and was already invoked millions of times daily when they published their work in 2018. That effort has since grown across AWS; later work describes scaling to a billion SMT queries per day.

The idea was to use formal methods, specifically a theorem solver- to formally model IAM, S3, and EC2 policies. Once we have these policies and their interactions modeled in formal logic, we could construct a proof that our invariants (things that we expect to be true) hold up. This ended up being quite successful, and has the added benefit that after the intensive task of modeling complex policies in formal logic, the actual queries across them could be made quite fast and scaled horizontally across compute.

The same problem, now with agents

Today, our challenges are quite similar. An agent, or a system of agents, each have filesystem, network, credential, tool, and MCP policies- each with different capabilities, and that can be combined together as agents can communicate with different agents.

Frontier labs have advocated for a trusted AI agent review of agent actions from specialized models, escalating the most important events for human approval and reducing approval fatigue. However, AI models- just like humans, are probabilistic and can miss important details. Even more, reviewing every agent action with an equally intelligent reviewer model, doubles your compute costs and effectively halves your total token throughput.

What we have been experimenting with and validating with OpenShell, is the use of formal methods to model and flexibly “prove” that certain invariants in a policy- such as an unintended way to bypass a rule blocking a write to a code repo, or a delete to a production database- are possible. What we found is that while modeling these policies can be complex, and must be kept up to date- there are some really powerful advantages.

• Ability to formally audit or prove invariants at any time
• Deterministic “proof” against our understanding of the policy
• These checks run in the order of milliseconds, no tokens required

These logic checks do not understand context- for example requesting access to delete a temporary, throw-away repository vs a production repository. But, combined with a human or trusted AI reviewer, these proofs can both provide a formal auditing trail required for running in sensitive, physical (real world), or regulatory controlled environments, AND can provide incredible value to a probabilistic AI reviewer with output that can’t be fooled or misdirected.

What does a proof over your policy definition buy you?

We view formal methods as a very promising area of research into agent control. See more on these proofs in action in adversarial research experiments here: https://nvidia.github.io/OpenShell-Research/dev-notes/posts/2026-08-27-adversarial-policy-review-long-horizon-agents/

Formal methods have not just been used for policy verification, they have a long history in critical systems- anywhere from flight control systems, core internet switching and routing, to the package managers that we use every day on our systems to ensure that complex dependencies between software on our systems are matched correctly.

For many AI researchers, some of us may have taken a class on formal verification in college, but comparatively few have used formal verification in practice. For the remainder of this post, we’ll explore an introduction to algorithmic verification and build a minimal example for agent control in OpenShell from the ground up, using a popular open-source solver.

SAT, SMT, and Z3 in five minutes

In computer science and formal methods, a SAT (satisfiability) solver answers whether a Boolean formula is satisfiable. If there are possible values of variables (let’s say x and y) that are true, the SAT solver returns true. If not, it returns false.

Given variables such as a and b, it can find an assignment that makes this formula true:

In contrast, an SMT (satisfiability modulo theories) solver extends that style of reasoning with theories: integers, real numbers, strings, regular languages, arrays, bit-vectors, and other useful domains.

Z3 is an SMT solver and theorem prover that has been developed and maintained by Microsoft Research. Z3 is general, and we need to build code to map the elements of our specific agent policy to the constructs that Z3 understands.

For example:

• ports are integers;
• hosts and paths are strings;
• Globs like *, **, or /.*/** can be represented as regular expressions;
• policy composition becomes Boolean logic.

The Z3 Guide is the best reference once the examples below feel familiar.

A few constructs cover most of what we need:

Construct	Meaning	OpenShell example
Sort	A type of value	String for a host, Int for a port
Symbol	A value Z3 is free to choose	the unknown action's method or path
Constraint	A formula that must hold	1 <= port <= 65535
And, Or, Not	Logical composition	candidate allows and maximum does not
String/regex theory	Constraints over text and languages	a path belongs to a compiled glob
Solver assertion	Adds a required formula	assert the existence of a violation
sat	A satisfying assignment exists	there is an action outside the maximum
Model	One satisfying assignment	a concrete binary, host, method, and path
unsat	No satisfying assignment exists	containment is proved for the model
unknown	Z3 did not establish either result	fail closed and request review/support

The direction of the query is important.

We do not ask Z3 to prove this:

proposed policy addition is safe

We have to model the question formally, and answer a very specific question. For example, one of the more general and useful proofs we have modeled in Z3 for this use case asks if a proposed policy can do any actions that a expert pre-defined policy (for example, Github read-only) cannot do. To go back to our earlier example with OpenClaw attempting to bypass layer 7 REST policy inspection, by combinign the access token with a binary using a layer 4 wire protocol, we would have encoded in Z3 that layer 4 capabilities exceed the capabilities of layer 7. Therefore, the combination of a credential (GitHub) plus a binary and network access over layer 4 exceeds the previously allowed combination of the same credential + the ‘gh’ binary over Layer 7 (REST). The prover would immediately catch this and flag a warning.

The query in this case looks like this-

proposed_policy_allows(action)
AND NOT safe_policy_allows(action)

Or the same property can be written as a set difference:

Allowed(candidate) ∖ Allowed(safe_policy) = ∅

If the solver returns sat, the difference is non-empty- meaning that there exist capabilities in the proposed policy that do not exist in the pre-approved reference policy.

If it returns unsat, no modeled counterexample exists, meaning that none of our invariants (assumptions) were violated. Let’s try writing a query like this ourselves.

A first containment query

Here is a small example in Z3's native SMT-LIB format. Save it as containment.smt2 and run:

The example compares two candidate policies against the same maximum.

(declare-const binary String)
(declare-const host String)
(declare-const port Int)
(declare-const layer String)
(declare-const method String)
(declare-const path String)

; The action domain: every request is either raw L4 or inspected REST.
(assert (or (= layer "l4") (= layer "rest")))

; An enforced REST rule covers only inspected REST traffic.
(define-fun maximum-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (= layer "rest")
       (= method "GET")
       (str.prefixof "/repos/NVIDIA/OpenShell/issues/" path)))

(define-fun broad-candidate-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (= layer "rest")
       (= method "POST")
       (str.prefixof "/repos/NVIDIA/" path)))

(define-fun narrow-candidate-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (= layer "rest")
       (= method "GET")
       (= path "/repos/NVIDIA/OpenShell/issues/123")))

; A raw L4 rule to the same host and port has no method or path to inspect.
; It covers L4 *and* anything that could ride over it, including REST.
(define-fun l4-candidate-allows () Bool
  (and (= binary "/usr/bin/gh")
       (= host "api.github.com")
       (= port 443)
       (or (= layer "l4") (= layer "rest"))))

; Check 1: does the broad candidate exceed the maximum?
(push)
(assert (and broad-candidate-allows (not maximum-allows)))
(check-sat)
(get-value (layer method path))
(pop)

; Check 2: Does the narrow candidate (GET, one issue) exceed the maximum?
(push)
(assert (and narrow-candidate-allows (not maximum-allows)))
(check-sat)
(pop)

; Check 3: Does the raw L4 rule to the same host and port exceed the maximum?
(push)
(assert (and l4-candidate-allows (not maximum-allows)))
(check-sat)
(get-value (layer method path))
(pop)

The first check returns sat, and the get-model above returns the witness below- a write to the root of the org that the safe (maximal) policy never permitted.

sat                                                  ; check 1: broad candidate
((layer "rest") (method "POST") (path "/repos/NVIDIA/"))
unsat                                                ; check 2: narrow candidate
sat                                                  ; check 3: raw L4
((layer "l4") (method "") (path ""))

The second check returns unsat. Every action the narrow candidate allows is already allowed inside the maximum. The third check is the OpenClaw story from earlier. The layer 4 candidate names the same host and port as is in our reference maximum policy, but over layer 4, which uses a wire protocol that cannot be enforced by OpenShell. The prover returns sat with layer = l4 and an empty method and path. In this case, we didn’t have to explicitly write a rule saying that L4 is broader than L7 REST, it effectively falls out of the encoding.

How to encode the full OpenShell policy as formal logic

OpenShell’s runtime prover models the following attributes for any network action:

action = {
  binary: String,
  host: String,
  port: Int,
  layer: String,
  method: String,
  path: String
}

Note: the example action above is just a subset, the OpenShell runtime also covers filesystem, process, credential, and inference containment.

We use code written in Rust to encode any policy changes proposed by agents into actions that can be checked by Z3. Once encoded, we can run a variety of checks. The first, a very general check- asks if the candidate (proposed) policy can do anything that the reference (safe) policy cannot do.

let candidate_allows = policy_allows(candidate, &action);
let maximum_allows = policy_allows(maximum, &action);

solver.assert(Bool::and(&[
    candidate_allows,
    !maximum_allows,
]));

match solver.check() {
    SatResult::Unsat => MaximumPolicyCheck::WithinMax,
    SatResult::Sat => {
        let model = solver.get_model().expect("sat result has a model");
        let counterexample = counterexample_from_model(&model, &action)
            .expect("model contains a symbolic action");
        MaximumPolicyCheck::ExceedsMax { counterexample }
    }
    SatResult::Unknown => MaximumPolicyCheck::Unsupported {
        reason: "Z3 returned unknown".to_owned(),
    },
}

Conceptually:

policy_allows(a) = ⋁ rule_allows(rule, a)

rule_allows(rule, a) =
  binary_matches(rule, a) ∧ endpoint_matches(rule, a)

This is where you start to see some of the complexity of modeling an entire policy language. For example, OpenShell supports * and ** glob semantics. These are compiled into Z3 regular expressions. As humans that are familiar with glob mechanics, we know that a single * cannot cross / for paths or . for hosts- while ** can. So, we use our Rust code to encode this logic. Z3's regular-expression theory can then check for us whether the symbolic string belongs to the resulting language. That scope is deliberate: OpenShell models a regular-language fragment rather than arbitrary language-specific regular expressions with features such as backreferences, and unsupported policy surfaces fail closed. For a deep-dive on our research around containment, check out the OpenShell spike on maximum policies and narrowness budgets here: https://github.com/NVIDIA/OpenShell/blob/spike/maximal-policy-prover-subset/crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md.

Expert queries are just more formulas!

In the examples above, we have used a very general and extensible query, essentially asking if one proposed policy, however complex it is, is a subset of another safe policy that we have already reviewed. But, once we have the policy language modeled in Z3, we can ask about anything we want to.

OpenShell’s policy advisor has four expert security checks built in, that run on any proposed policy and that are provided to the human or agent reviewer for approval. In adversarial testing, we have found that providing the results of these checks- which cannot be fooled, manipulated, or defeated directly, as context to an agent reviewer as an incredibly valuable way to increase the trustworthiness of agentic or human reviewers. Read more here: https://docs.nvidia.com/openshell/sandboxes/policy-advisor.

Today, the OpenShell policy prover encodes the following expert queries which run on every proposed policy before approval. From the docs:

Category	Triggered when
link_local_reach	A rule reaches 169.254.0.0/16, fe80::/10, or a known metadata hostname.
l7_bypass_credentialed	A binary using a wire protocol the L7 proxy cannot inspect (git-remote-https, ssh, nc) gains reach to a host where a credential is in scope.
credential_reach_expansion	A binary gains credentialed reach to a (host, port) it could not reach before.
capability_expansion	On a (binary, host, port) that already had credentialed reach, the proposal adds a new HTTP method. The finding cites the specific method.

Conclusion

We’re incredibly excited about the promise of formal methods to help govern, audit, and build trustworthiness with agents over long horizon and continuously expanding and important tasks. If you’re working with formal methods, or interested in contributing to OpenShell- please reach out to us on the CNCF Slack, or join our weekly community meetings (sign up at https://github.com/NVIDIA/OpenShell).

Resources

Definitive references for Z3, once the examples above start to feel familiar

DeepMind’s verified code generation approach to the same problem-

Blogs on AI review of agent permissions

openshell formal-methods z3 agents security