We started exploring formal methods in OpenShell while working through a
practical problem: how should a long-running agent request more authority after
its policy blocks an action?
OpenShell runs agents in policy-controlled sandboxes that can constrain network
endpoints, credentials, filesystem access, methods, paths, and protocol-specific
operations. In our experiments, policy denials often arrived partway through a
task, when the agent had enough context to explain what it needed and draft a
possible change. We could send every proposal to a human or model, but we wanted
to understand which part of the decision could be checked mechanically.
Our first prototype focused on policy containment. If an operator defines the
maximum authority an agent may obtain, the gateway can compose the policy that
would result from a proposed change and ask:
Allowed(candidate) ⊆ Allowed(maximum)?
The candidate is the fully composed policy after the change. The maximum is an
operator-controlled ceiling; it does not grant access by itself. Implementing
this check showed us why reviewing one proposed rule at a time was not enough. A
request for one GitHub endpoint could grant every method under a wildcard path,
raw L4 access could bypass REST, GraphQL, or MCP inspection, and a reasonable
rule could combine with existing rules to create broader authority.
We encoded those policy semantics in [Z3](https://microsoft.github.io/z3guide/)
and asked it to search for an action the candidate allowed but the maximum did
not. A counterexample showed us the specific binary, endpoint, method, or path
outside the boundary. If Z3 could not find one, containment held for the
semantics represented in the model. That gave us inspectable evidence rather
than a general risk score.
We also learned that proof and contextual judgment work best together. The
agent's request and the prover's full findings go to a model or human reviewer.
The request provides task context, while the prover shows whether the encoded
policy invariants hold or supplies a concrete counterexample when they do not.
That helps the reviewer catch an unexpected interaction buried in the composed
policy that the agent or reviewer might otherwise miss.
This post walks through the containment query, how we modeled OpenShell policy
in Z3, where that model stops, and what we are learning from experiments with
least-privilege budgets for agent-authored policy changes.
## Formal methods, at the scale of one decision
Formal methods cover a large family of techniques for describing systems and
properties mathematically and then reasoning about whether those properties
hold. Model checking, theorem proving, abstract interpretation, SAT solving,
and SMT solving all fall under that umbrella.
For the problem here, we only need four pieces:
- **A model:** a precise representation of the actions a policy permits.
- **A property:** for example, “the candidate grants no action outside the managed
maximum.”
- **A decision procedure:** Z3 searches for an assignment that satisfies the
logical query.
- **An enforcement point:** the gateway acts on the result before committing the
policy change.
The guarantee is relative to those pieces.
If the model omits a policy field, the proof says nothing about that field. If
the runtime and prover interpret a glob differently, they disagree about the
boundary. If an agent has another path to the same effect, proving one admission
decision correct does not give you complete mediation.
So “formally verified” does not mean “the system is safe.” For this use case, it
means something narrower: under the policy semantics represented in the model,
the solver could not find an action that violates the property we asked it to
check.
That narrow statement is useful- A model reviewing a permission request can be
influenced by the request's wording, miss an interaction, or make different
decisions on two similar inputs. Z3 evaluates the formula it receives. The
parts that deserve scrutiny are explicit: the specification, its encoding, the
handoff from proof to commit, and the runtime enforcement semantics.
## SAT, SMT, and Z3 in five minutes
A SAT solver answers whether a Boolean formula is satisfiable.
Given variables such as `a` and `b`, it can find an assignment that makes this
formula true:
```text
a AND (NOT b)
```
An SMT 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 developed by Microsoft Research. Its
supported theories map conveniently to policy models:
- ports are integers;
- hosts and paths are strings;
- globs can be represented as regular expressions;
- policy composition becomes Boolean logic.
The [Z3 Guide](https://microsoft.github.io/z3guide/) 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:
```text
candidate is safe
```
We ask it to find a violation:
```text
candidate_allows(action)
AND NOT maximum_allows(action)
```
The same thing can be written as a set difference:
```text
Allowed(candidate) ∖ Allowed(maximum) = ∅
```
If the solver returns `sat`, the difference is non-empty and its model gives us
a concrete member.
If it returns `unsat`, no modeled counterexample exists.
## A first containment query
Here is a small example in Z3's native SMT-LIB format. Save it as
`containment.smt2` and run:
```console
z3 containment.smt2
```
The example compares two candidate policies against the same maximum.
```smt2
(declare-const binary String)
(declare-const host String)
(declare-const port Int)
(declare-const method String)
(declare-const path String)
(define-fun maximum-allows () Bool
(and (= binary "/usr/bin/gh")
(= host "api.github.com")
(= port 443)
(= 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)
(= method "POST")
(str.prefixof "/repos/NVIDIA/" path)))
(define-fun narrow-candidate-allows () Bool
(and (= binary "/usr/bin/gh")
(= host "api.github.com")
(= port 443)
(= method "GET")
(= path "/repos/NVIDIA/OpenShell/issues/123")))
(push)
(assert (and broad-candidate-allows (not maximum-allows)))
(check-sat)
(get-model)
(pop)
(push)
(assert (and narrow-candidate-allows (not maximum-allows)))
(check-sat)
(pop)
```
The first check returns `sat`.
One possible model is:
```text
method = "POST"
path = "/repos/NVIDIA/"
```
That action is permitted by the broad candidate and not by the read-only
maximum.
The narrow candidate returns `unsat`: its exact GET request is contained by the
maximum.
`push` and `pop` create temporary solver scopes. They are convenient when
several related queries share one base model. OpenShell's current containment
function creates a fresh solver for each containment query; some earlier
verification experiments used incremental scopes to run several risk queries
over the same reachability model.
There is also no explicit `exists` in the source.
Because `binary`, `host`, `port`, `method`, and `path` are declared without fixed
values, Z3 is free to choose them. Operationally, satisfiability is answering:
```text
exists action:
candidate_allows(action)
AND NOT maximum_allows(action)
```
Avoiding explicit quantifiers where possible keeps the SMT model simpler and
tends to make solver behavior easier to reason about.
## Encoding OpenShell policy as formal logic
OpenShell models one symbolic network action:
```text
action = {
binary: String,
host: String,
port: Int,
layer: String,
method: String,
path: String
}
```
Rust parses and normalizes the policy schema, then builds two Boolean predicates
over the same symbolic action:
```text
candidate_allows(action)
maximum_allows(action)
```
At the center of the containment check is essentially:
```rust
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(),
},
}
```
The policy itself becomes nested conjunctions and disjunctions.
Conceptually:
```text
policy_allows(a) = ⋁ rule_allows(rule, a)
rule_allows(rule, a) =
binary_matches(rule, a) ∧ endpoint_matches(rule, a)
```
An endpoint constrains the host and port. When L7 inspection is active, it also
constrains things such as methods and paths.
OpenShell supports `*` and `**` glob semantics. These are compiled into Z3
regular expressions. A single `*` cannot cross the relevant separator — `/` for
paths or `.` for hosts — while `**` can. Z3's regular-expression theory then
checks whether the symbolic string belongs to the resulting language.
This matters because the network layer is part of the authority being proved.
Raw L4 authority over a binary, host, and port is broader than inspected L7
authority over the same connection. L4 does not preserve REST methods and
paths, GraphQL operations and fields, or MCP tools and resources. A raw network
grant can therefore include actions that would have been excluded by
protocol-specific controls.
That interaction is easy to miss when reviewing one rule at a time. In the
logical model, the two grants denote different sets of actions.
## A managed maximum
We use the containment query as the basis for a managed maximum.
The maximum is owned by the gateway and acts as a ceiling. It does not grant the
sandbox access by itself.
Before creating a sandbox or committing an authority-changing update, the
gateway evaluates the fully composed sandbox and provider policy against that
ceiling.
For an agent-authored proposal, the result can be:
- **Apply:** the proposed authority is inside the maximum's auto-eligible region.
- **Ask:** it is inside the maximum but intersects authority marked for review,
or the sandbox is running in managed ask mode.
- **Reject:** it exceeds the maximum or depends on a policy surface the prover
does not support.
The gateway recomputes containment against live policy and provider state
immediately before persistence.
That last step matters. A proposal that passed earlier is evidence that a
particular state was acceptable; it is not a reusable capability token.
## What we learned to model
Our first OpenShell experiments asked targeted questions: could a binary reach
link-local metadata, did a proposal expand credential-bearing reach, could raw
L4 access bypass L7 inspection, or did it add methods to an already reachable
endpoint?
Those checks were useful because they encoded security expertise and produced
concrete evidence for reviewers. As we worked with them, we found two patterns
worth separating.
The first was general policy comparison. A maximum-boundary check asks whether
a candidate remains inside an operator-defined ceiling. A narrowness check asks
how much authority the candidate adds relative to the action that caused the
denial. Both apply broadly to agent permission changes without requiring us to
predict every possible misuse.
The second was the value of domain-specific invariants. Subject-matter experts
often know the properties they care most about preserving: an agent must not
reach a metadata service, bypass required L7 inspection, or gain a credentialed
mutation path to a protected resource. Encoding those properties in logic lets
the prover search for a concrete counterexample as the policy changes.
We saw this in our [long-horizon adversarial experiment](./2026-08-27-adversarial-policy-review-long-horizon-agents.md).
An agent proposed a GitHub write permission bound to an apparently constrained
process. The prover reported the resulting credential-reach expansion, helping
the reviewer recognize that the proposal still enabled the protected write.
One practical lesson was to make each result's role explicit. Some invariants
should prevent a change outright. Other findings are better presented as
context for a reviewer. The managed maximum provides the general boundary
around both.
The other lesson was to keep the scope of the proof visible. Our initial model
covered L4, REST, and WebSocket authority, while unsupported GraphQL and MCP
surfaces failed closed. The current containment path also covers filesystem
paths, although that comparison is implemented directly in Rust. GraphQL, MCP,
query matchers, and CIDR-based `allowed_ips` still require additional modeling
before a containment result can make claims about them.
## Can least privilege have a budget?
Containment tells us whether a candidate stays below the maximum.
It does not tell us whether the candidate is a good response to the denial that
caused the agent to request more access.
Suppose the maximum allows read access across an organization's GitHub
repositories. An agent needs to read one issue and proposes:
```text
GET /repos/NVIDIA/**
```
That proposal may be fully contained by the maximum while still being much
broader than the task required.
We have started experimenting with a second comparison:
```text
delta(action) =
candidate_allows(action)
AND NOT current_policy_allows(action)
```
For each proposed grant, Z3 can determine whether it adds new authority and
return a representative new action.
The current spike then evaluates the shape of that grant in Rust.
An exact addition can have a low cost. A wildcard costs more. A recursive `**`
costs more again. Replacing inspected L7 authority with raw L4 access carries a
much larger cost.
A conservative budget could permit one exact addition while routing broader
changes to review.
This is deliberately a hybrid.
Z3 is not measuring the cardinality of an often-infinite action set. It
establishes that semantic expansion exists and can produce examples of that
expansion. The budget is a product policy over structural features of the
proposed grant.
Whether those features and weights correspond well enough to operational risk
is something we still need to test.
Maximum containment is further along as an admission boundary. Least-privilege
budgets are an experiment.
A few questions we want to explore:
- Can denials and solver counterexamples help agents draft narrower policy
changes on the next attempt?
- Can we define useful notions of semantic breadth for GraphQL operations and
MCP tools without reducing them to fragile syntax scores?
- How should many individually small permission changes accumulate over a
long-running task or a tree of delegated agents?
## Where models still belong
A containment proof only answers the question encoded in the property.
It does not know why an agent wants access. It does not know whether the user's
request makes an action appropriate. It cannot weigh business context,
reversibility, or unusual combinations that were never represented in the
model.
Those are reasons to keep model-based and human review in the system.
An approval flow we are exploring looks roughly like this:
There is precedent for combining these kinds of mechanisms.
[OpenAI](https://openai.com/business/guides-and-resources/a-practical-guide-to-building-ai-agents/#building-guardrails)
describes combining model-based and rules-based guardrails.
[Anthropic's work on trustworthy agents](https://www.anthropic.com/research/trustworthy-agents)
treats safety as a property of the model, harness, tools, and environment
together. [Google DeepMind's VeriGuard](https://arxiv.org/abs/2510.05156)
similarly places verification between proposed agent behavior and execution.
Our working rule is simple: use a formal check when the boundary can be stated
precisely, and do not ask the formal model to answer questions it was not built
to represent.
Likewise, a contextual reviewer should not silently override a hard invariant
just because the request sounds convincing.
Keeping those roles explicit makes the resulting authority easier to reason
about.
## Start with one decision
The core containment query is small:
```text
candidate_allows(x)
AND NOT maximum_allows(x)
```
You do not need to begin by formally specifying an entire agent or proving a
neural network correct. Pick one consequential decision with inputs you can
model, write down one property you want to preserve, and put the check somewhere
that can actually enforce the result.
For OpenShell, that decision is whether an agent may change its own sandbox
authority.
SMT solving gives us a different artifact from another review of the request:
either a counterexample showing authority outside the maximum, or a proof that
no such action exists under the modeled semantics.
There is plenty we have not modeled yet, and least-privilege budgeting is still
an experiment. That is part of what makes this area useful to work on in the
open.
If you are building agent policies, tool permissions, or another constrained
action surface, try writing down the action space explicitly and asking the
solver for the counterexample.
Sometimes the useful part of formal methods is not proving a large system
correct. It is making one boundary precise enough that the system can answer for
itself.
## Resources
- [Z3 Guide](https://microsoft.github.io/z3guide/)
- [Z3: An Efficient SMT Solver](https://www.microsoft.com/en-us/research/?p=825739)
- [Z3 regular expressions](https://microsoft.github.io/z3guide/docs/theories/Regular%20Expressions/)
- [Z3 source and language bindings](https://github.com/Z3Prover/z3)
- [VeriGuard: Enhancing LLM Agent Safety via Verified Code Generation](https://arxiv.org/abs/2510.05156)
- [Trustworthy agents in practice](https://www.anthropic.com/research/trustworthy-agents)
- [A practical guide to building AI agents](https://openai.com/business/guides-and-resources/a-practical-guide-to-building-ai-agents/)
