OpenShell/docs/reference/policy-prover.mdx

---
# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
# SPDX-License-Identifier: Apache-2.0
title: "Standalone Policy Prover"
sidebar-title: "Policy Prover"
description: "Install and use the standalone OpenShell policy prover to check a local candidate policy against a managed boundary."
keywords: "Generative AI, Cybersecurity, Policy, Prover, Boundary, Containment, CI"
position: 4
---

`openshell-prover` checks whether the authority in a local candidate policy is
contained within a local boundary policy. The command reads files from the host
and does not connect to an OpenShell gateway.

The candidate must be the fully composed effective policy after the proposed
change, including any provider-contributed authority. The boundary is an
operator-owned ceiling. It does not grant authority by itself.

## Install the Prover

The standard OpenShell installer includes `openshell-prover`:

```shell
curl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | sh
openshell-prover --version
```

The prover remains independent of the gateway at runtime. If you only need the
standalone binary, use the artifacts listed in the
[Support Matrix](/reference/support-matrix#standalone-policy-prover). These
artifacts and `openshell-prover-checksums-sha256.txt` are attached to
[OpenShell releases](https://github.com/NVIDIA/OpenShell/releases).

The release archive includes the solver linkage required by the executable.
It does not require the main `openshell` command, a gateway configuration, or
a separate Z3 installation.

## Check a Policy Boundary

Create `boundary.yaml` with this boundary policy:

```yaml
version: 1
filesystem_policy:
  read_only:
    - /usr
    - /etc
```

Create `candidate.yaml` with this contained candidate:

```yaml
version: 1
filesystem_policy:
  read_only:
    - /usr
```

Run the check:

```shell
openshell-prover check candidate.yaml --boundary boundary.yaml
```

A contained candidate prints `result: within_boundary` and exits with status `0`.
To see an exceeding result and its counterexample, replace `candidate.yaml`
with a policy that grants writes to `/tmp`. The boundary grants no write
access:

```yaml
version: 1
filesystem_policy:
  read_only:
    - /usr
  read_write:
    - /tmp
```

```shell
openshell-prover check candidate.yaml --boundary boundary.yaml
```

To check the current effective policy of an existing sandbox, export it without
display metadata:

```shell
openshell sandbox get my-sandbox --policy-only > candidate.yaml
openshell-prover check candidate.yaml --boundary boundary.yaml
```

This export includes provider-contributed rules. For a proposed change that is
not active, supply the complete post-change effective policy. The standalone
prover does not compose a base policy with provider rules.

Use JSON when a script consumes the result:

```shell
openshell-prover check candidate.yaml \
  --boundary boundary.yaml \
  --output json
```

The JSON object includes the result, exit code, input paths, schema version,
prover version, and modeled domains. `schema_version` versions the JSON contract,
`prover_version` identifies the implementation that produced the result, and
`coverage.domains` is the machine-readable declaration of modeled policy
domains. An exceeding result also includes a typed counterexample. Automation
should use `result` and `reason_code` instead of parsing the human-readable
explanation.

| Field | When populated |
|---|---|
| `counterexample` | An object for `exceeds_boundary`; otherwise `null`. |
| `reason_code` | A stable identifier for an emitted `error`, `unsupported`, or `inconclusive` result; otherwise `null`. |
| `reason` | A human-readable explanation paired with `reason_code`; otherwise `null`. |

The `counterexample.domain` field selects one of these objects:

| Domain | Fields |
|---|---|
| `filesystem` | `access` (`read` or `write`) and `path`. |
| `process` | `field` (`run_as_user` or `run_as_group`), `boundary`, and `candidate`. |
| `landlock` | `boundary` and `candidate` compatibility modes. |
| `network` | `binary`, `ancestor_binary`, `binary_identity_required`, `host`, `destination_ip`, `trusted_gateway`, `port`, `protocol`, `method`, and `path`. |

Network `binary` and `ancestor_binary` values are `null` when binary identity
enforcement is disabled. `method` and `path` are `null` for L4 witnesses.
`trusted_gateway: true` means the witness uses a recognized host-gateway alias
with a runtime-provided trusted gateway binding; `false` uses ordinary
destination validation.

The stable reason codes are `invalid_input`, `unsupported_policy_shape`,
`unresolved_workdir`, `unresolved_binary_path`,
`unresolved_filesystem_path`, `solver_timeout`, `solver_unknown`,
`resource_limit`, `invalid_witness`, and `cancelled`.

The solver has a finite 10-second default budget. Set a different positive
budget with an integer followed by `ms`, `s`, or `m`:

```shell
openshell-prover check candidate.yaml \
  --boundary boundary.yaml \
  --timeout 30s \
  --output json
```

## Exit Codes

| Exit | Result | Meaning |
|---|---|---|
| `0` | `within_boundary` | Containment was established for the reported modeled domains. |
| `1` | `exceeds_boundary` | The candidate exceeds the boundary; inspect the counterexample. |
| `2` | `error` | Arguments, input files, policy syntax, or command execution prevented a valid check. |
| `3` | `unsupported` or `inconclusive` | The model cannot soundly cover the policy shape, or the solver did not reach a determination. |
| `130` | `inconclusive` when graceful handling completes | The user interrupted the command with Ctrl-C on Unix; a second or very early interruption may prevent output. |

Only exit `0` means the verification succeeded. Treat unsupported and
inconclusive results as failures in CI.

## Interpretation and Limits

The containment check covers filesystem paths, process identity settings,
Landlock compatibility requirements, L4 destination authority, and enforced
REST method and path authority, including explicit REST denies. The result
object reports the policy domains modeled by each check. Policies that use
recognized authority outside that coverage return `unsupported` rather than
silently ignoring it.

Both inputs use the same bounded YAML/JSON parser and authored policy schema as
OpenShell. Unknown fields, duplicate keys, malformed field types, and unsupported
managed `metadata` or `review` annotations return `error` with
`reason_code: invalid_input` and exit `2`. Schema-valid controls outside the
containment model return `unsupported` and exit `3`.

The prover applies aggregate limits across the candidate and boundary before
semantic shape validation: 1,024 network rules, 4,096 endpoints, 4,096 binary
selectors, 65,536 authored port entries, 4,096 `allowed_ips` entries, 16,384
REST rules, 4 KiB per modeled pattern, and 1 MiB of modeled pattern text.
Exceeding any limit returns `inconclusive` with `reason_code: resource_limit`.
A cancellation already requested at preflight takes precedence over that
result; otherwise a resource limit takes precedence over unsupported
policy-shape diagnostics. This ordering keeps validation work bounded for
checked-in CI inputs.

### Process and Landlock settings

Matching supported `run_as_user` and `run_as_group` values do not expand the
configuration. Changing an explicit non-root identity to `root` or `0` returns
`exceeds_boundary` with the field and both values. Other identity changes return
`unsupported`; the command does not resolve accounts from a sandbox image.
These comparisons assume consistent identity resolution and execution settings.
They do not prove permission relationships between arbitrary Linux accounts.

Landlock `hard_requirement` may not become `best_effort`. That change returns
`exceeds_boundary`. Keeping the same mode or strengthening it to
`hard_requirement` passes this part of the check. This compares the requested
requirement, not whether a target kernel successfully installed Landlock
restrictions.

### Destination IP restrictions

The network action includes an IPv4 or IPv6 destination address. CIDR entries
in `allowed_ips` are modeled together with host, port, executable, and REST
restrictions; network counterexamples include `destination_ip`. An empty IP
list follows the runtime's destination rules and is not a universal allowlist.
The check does not resolve DNS on the host running the CLI.

Policies whose potentially overlapping endpoints select different destination
restrictions remain unsupported because the runtime uses the selected
endpoint's address filter. The prover conservatively treats wildcard host
selectors on a shared port as potentially overlapping, including when their
literal suffixes differ. CIDR unions within a supported endpoint are checked by
the solver. Unsupported IP-literal wildcard selectors and ranges rejected by
the runtime also cannot produce a successful proof.

Consumers must inspect `coverage.domains` and require every domain relevant to
their authorization decision. A successful result applies only to those
reported domains and the documented assumptions.

### Remaining limits

Network binary selectors, endpoint host and path selectors, and REST allow and
deny method and path selectors must use ASCII literals in both the candidate and
boundary. A non-ASCII literal in one of these fields returns `unsupported` with
`reason_code: unsupported_policy_shape`, including when it appears only in a
deny. Embedded NUL bytes in these fields are also unsupported. This is a
prover-model limitation, not a general policy validation rule: filesystem paths
and unrelated policy text retain their existing Unicode behavior. ASCII
wildcard selectors still cover non-ASCII runtime values matched by the policy
engine.

Containment means `Allowed(candidate)` is a subset of `Allowed(boundary)` under
the reported model. It does not establish least privilege, automatic approval
eligibility, semantic safety, or equivalence to a running sandbox's kernel
state. In particular:

- The command does not fetch the current sandbox policy or compose provider
  rules. The caller must supply the effective candidate.
- The command does not apply, approve, or persist a policy.
- Environment-dependent authority, such as an unresolved image workdir,
  returns `unsupported` when the result depends on that missing context.
- Binary comparisons that can change when an image resolves an exact selector
  through a symlink return `unsupported`. This covers exact candidate grants
  under boundary globs and exact boundary denies replaced by candidate globs.
  Use matching exact canonical paths when possible.
- Policies with overlapping L4 and enforced REST endpoints return
  `unsupported` because inspection selection depends on the complete set of
  matching runtime endpoint configurations.
- Network containment checks both supported runtime configurations: binary
  identity enforcement enabled and disabled. When enabled, grants and denies
  match the executable or an ancestor identity. Network counterexamples report
  the configuration and identities that expose the additional authority.
- REST containment witnesses use canonical request methods and paths.
- If a solver string cannot be decoded and validated faithfully, the command
  returns `inconclusive` with `reason_code: invalid_witness` instead of emitting
  a counterexample.
- Both files are interpreted in the same sandbox filesystem namespace and
  mount model, with stable path resolution when enforcement rules are created.
  The CLI does not resolve sandbox paths against the host.
- Filesystem containment supports removing grants and reducing write grants to
  read-only grants at matching paths. A boundary grant for `/` also covers other
  paths for the same access. Comparisons between different paths otherwise
  return `unsupported` with `reason_code: unresolved_filesystem_path`: a lexical
  child can resolve outside its parent through a symlink, and unrelated paths
  can resolve to the same object. This includes narrowing `/tmp` to `/tmp/cache`.
  If the boundary grants no access of the requested kind, adding that access
  returns `exceeds_boundary`.

Use the [Policy Schema Reference](/reference/policy-schema) for the full policy
language. A successful prover result covers only the policy domains reported in
its evidence.