@@ -1,6 +1,6 @@
 # OpenShell Architecture
 
-OpenShell runs autonomous AI agents in sandboxed environments with explicit
+OpenShell runs fleets of autonomous AI agents in sandboxed environments with explicit
 policy, credential, identity, and network boundaries. The target architecture is
 built around three stable runtime components: the **CLI**, the **Gateway**, and
 the **Supervisor**.
@@ -29,6 +29,7 @@ flowchart TB
 
     subgraph CP["Control Plane"]
         GW["Gateway core"]
+        PROVER["Policy prover"]
         DB[("Shared persistence")]
         COMPUTE["Compute"]
         CREDS["Credentials"]
@@ -59,6 +60,7 @@ flowchart TB
     TUI -->|"gRPC / HTTP"| GW
 
     GW --> DB
+    GW -->|"proposed policy changes"| PROVER
     GW --> COMPUTE
     GW --> CREDS
     GW --> CPIDENT
@@ -89,6 +91,7 @@ flowchart TB
 |---|---|
 | CLI, SDK, TUI | User-facing management surfaces. They talk to the gateway and do not need to know which infrastructure drivers are active. |
 | Gateway | Authenticated control plane, API server, durable state, policy and settings delivery, provider config, supervisor session ownership, and relay coordination. |
+| Policy prover | Gateway-linked formal verification of proposed policy changes. It reports categorical findings (new credentialed reach, new HTTP methods, L7 bypass, link-local reach); any finding blocks auto-approval. The same crate backs the standalone `openshell-prover check` boundary command, which runs on local files without a gateway. See [Security Policy](security-policy.md). |
 | Compute subsystem | Sandbox lifecycle semantics: creation, deletion, watching, reconciliation, and state transitions. Platform provisioning details belong to the compute driver. |
 | Credentials subsystem | Logical provider and credential resolution. Secret storage and platform-native credential access belong to credentials drivers. |
 | Control-plane identity | Authentication and authorization for users, operators, and API clients. External identity verification belongs to identity drivers. |
 
@@ -6302,6 +6302,7 @@ mod tests {
                 "google-vertex-ai",
                 "nvidia",
                 "openai",
+                "openrouter",
                 "pypi"
             ]
         );
 
@@ -11,8 +11,9 @@ position: 2
 ![OpenShell system architecture showing a trusted supervisor separated from a network-isolated sandbox workload. The workload can connect only to the supervisor.](../images/openshell-system-architecture.svg)
 
 OpenShell separates control-plane state from sandbox enforcement. The gateway
-owns sandbox state, policy, providers, and access. A compute driver provisions
-the workload and its isolation boundary.
+owns sandbox state, policy, providers, and access, and uses formal verification
+to evaluate proposed policy changes before they are approved. A compute driver
+provisions the workload and its isolation boundary.
 
 The trusted supervisor runs outside the workload. `openshell-sandbox` runs
 inside it, owns the agent process, and mediates its network requests. All other
@@ -25,10 +26,10 @@ gateway for configuration, credentials, logs, and interactive sessions.
 |---|---|
 | [Gateway](/how-it-works/gateways/overview) | Checks who you are and remembers everything about your sandboxes. It delivers policy and settings, attaches providers, decides who can do what, and coordinates connections into sandboxes. |
 | [Compute runtime](/how-it-works/sandboxes/runtimes) | Creates the sandbox, starts the supervisor and the workload, sets up the private channel between them, and builds the network fence. It reports status back and cleans up when the sandbox goes away. |
-| [Supervisor](#inside-the-sandbox-boundary) | Lives on the trusted side of the boundary. It checks requests against policy, supplies credentials, resolves DNS, opens approved connections, and keeps the link to the gateway alive. |
-| [Isolation backend](/extensibility/isolation-backends) | Gives the supervisor one consistent way to work with any runtime: confirm the boundary, start the agent, run commands, forward connections, and see network requests. |
-| [`openshell-sandbox`](#inside-the-sandbox-boundary) | Lives inside the boundary with the agent. It owns the agent's processes, knows which program made each request, applies process controls, and forwards TCP and DNS traffic to the supervisor. |
+| [Supervisor](#inside-the-sandbox-boundary) | Lives on the trusted side of the boundary. It checks requests against policy, supplies credentials, resolves DNS, opens approved connections, and keeps the link to the gateway alive. It works with every runtime through one [isolation backend](/extensibility/isolation-backends) interface to confirm the boundary, start the agent, run commands, forward connections, and see network requests. |
+| [OpenShell Sandbox](#inside-the-sandbox-boundary) | Lives inside the boundary with the agent. It owns the agent's processes, knows which program made each request, applies process controls, and forwards TCP and DNS traffic to the supervisor. |
 | [Outer network fence](/security/best-practices#deny-by-default-egress) | Denies all network egress from the workload except its protected connection to the supervisor. Each runtime builds this with its own native tools. |
+| [Policy prover](/how-it-works/policies/prover) | Runs in the gateway and uses formal verification to check each proposed policy change before approval. It flags changes such as new credentialed reach, new HTTP methods, or access to cloud metadata endpoints, and any finding blocks auto-approval. It also ships as the standalone `openshell-prover` command for checking a policy against a boundary in CI. |
 | [Policies](/how-it-works/policies/overview) | Describe what the agent can touch: files, processes, network destinations, API calls, and where provider credentials can go. |
 | [Providers](/how-it-works/providers/overview) | Connect a service name to a stored credential. The supervisor hands that credential out only where policy allows it. |
 
 
@@ -26,6 +26,43 @@ openshell status
 
 To install a specific release, set `OPENSHELL_VERSION` to a release tag. Release artifacts are also on the [GitHub Releases](https://github.com/NVIDIA/OpenShell/releases) page.
 
+## Prerelease and Development Builds
+
+Use a prerelease candidate to evaluate an upcoming release, or the rolling development build to test the latest commit on `main`. These builds may change before the next stable release. The matching documentation is published in the [development channel](https://docs.nvidia.com/openshell/dev/index.html).
+
+Prerelease packages are retained as GitHub Actions artifacts for 90 days and require an authenticated [GitHub CLI](https://cli.github.com/) session. The `pre` alias installs the latest prerelease:
+
+```shell
+gh auth login
+curl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | \
+  OPENSHELL_VERSION=pre sh
+```
+
+The installer checks prerelease tags from newest to oldest, selects an unexpired artifact from a successful release run for the current platform, and downloads only that artifact. Installed packages keep the candidate's exact version, such as `0.1.0-pre.3`. Prerelease tags do not create entries on the GitHub Releases page. On Linux, prereleases and explicit release tags use Debian or RPM packages even if `snap` is installed.
+
+The rolling [`dev` release](https://github.com/NVIDIA/OpenShell/releases/tag/dev) does not require GitHub authentication:
+
+```shell
+curl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | \
+  OPENSHELL_VERSION=dev sh
+```
+
+For Kubernetes, select the corresponding Helm chart version. Helm chart versions omit the leading `v` from release tags:
+
+```shell
+# Pin an exact candidate
+helm upgrade --install openshell \
+  oci://ghcr.io/nvidia/openshell/helm-chart \
+  --version 0.1.0-pre.3
+
+# Rolling development build
+helm upgrade --install openshell \
+  oci://ghcr.io/nvidia/openshell/helm-chart \
+  --version 0.0.0-dev
+```
+
+Prerelease charts use exact `<version>-pre.N` versions. Development charts are also published as immutable `0.0.0-dev.<commit-sha>` versions when you need to pin a specific commit.
+
 ## Supported Runtimes
 
 The local gateway auto-detects an available runtime. To pin one, set `compute_driver` in the gateway TOML file. See [Sandbox Runtimes](/how-it-works/sandboxes/runtimes).
 
@@ -3,12 +3,12 @@
 # SPDX-License-Identifier: Apache-2.0
 title: "Overview of NVIDIA OpenShell"
 sidebar-title: "Overview"
-description: "OpenShell is the safe, private runtime for autonomous AI agents. Run agents in sandboxed environments that protect your data, credentials, and infrastructure."
+description: "OpenShell is the safe, private runtime for fleets of autonomous AI agents. Run agents in sandboxed environments that protect your data, credentials, and infrastructure."
 keywords: "Generative AI, Cybersecurity, AI Agents, Sandboxing, Security, Privacy, Provider Credentials"
 position: 1
 ---
 
-NVIDIA OpenShell is an open-source runtime for executing autonomous AI agents in sandboxed environments with kernel-level isolation. It combines sandbox runtime controls and a declarative YAML policy so teams can run agents without giving them unrestricted access to local files, credentials, and external networks.
+NVIDIA OpenShell is an open-source runtime for executing fleets of autonomous AI agents in sandboxed environments with kernel-level isolation. It combines sandbox runtime controls and a declarative YAML policy so teams can run agents without giving them unrestricted access to local files, credentials, and external networks.
 
 <Note>
 New in OpenShell 0.1.0: a [stable release cadence](/about/support-matrix#releases), new [isolation primitives](/about/architecture), and an expanded [extension surface](/extensibility/overview), along with much more.
 
@@ -15,41 +15,36 @@ with the agent as its main process.
 **1. Configure what the agent has access to.**
 
 A [provider profile](/how-it-works/providers/profiles) defines the credentials, service
-endpoints, and executable paths an agent may use. For Claude Code, review the
-[example profile](https://github.com/NVIDIA/OpenShell/blob/main/providers/claude-code.yaml),
-including its executable paths for your image, then import it and
-[create a provider](/how-it-works/providers/overview#create-a-provider) that
-stores its credentials.
+endpoints, and executable paths an agent may use.
+
+This example runs OpenCode
+against OpenRouter. Review the
+[example profile](https://github.com/NVIDIA/OpenShell/blob/main/providers/openrouter.yaml),
+which allows `/usr/local/bin/opencode` to reach `openrouter.ai`, then import
+it and [create a provider](/how-it-works/providers/overview#create-a-provider)
+that stores its credentials.
 
 ```shell
 openshell profile import \
-  --url https://raw.githubusercontent.com/NVIDIA/OpenShell/main/providers/claude-code.yaml
+  --url https://raw.githubusercontent.com/NVIDIA/OpenShell/main/providers/openrouter.yaml
 
 openshell provider create \
-  --name claude-code \
-  --type claude-code \
+  --name openrouter \
+  --type openrouter \
   --from-existing
 ```
 
-Set `ANTHROPIC_API_KEY` before creating the provider. OpenShell stores its
-value in the credential store.
+Set `OPENROUTER_API_KEY` before creating the provider. OpenShell stores its
+value in the credential store and sends it only to `openrouter.ai`.
 
-**2. Configure the sandbox image.**
+**2. Choose the sandbox image.**
 
-Build or select a [sandbox image](/how-it-works/sandboxes/overview#sandbox-images)
-containing Claude Code and every tool it needs:
+Use any [sandbox image](/how-it-works/sandboxes/overview#sandbox-images) that
+contains the agent and every tool it needs.
 
-```shell
-docker build -t agent:local .
-```
+In this example, the OpenCode image installs `opencode` at `/usr/local/bin/opencode`.
 
-For a remote gateway, push the image to a registry that the gateway can pull
-from. Use an explicit version instead of a mutable tag for reproducible
-deployments.
-
-The built-in fallback policy grants access to the working directory and common
-runtime paths, and denies network egress unless an attached provider contributes
-an endpoint. Create a custom [sandbox policy](/how-it-works/policies/overview) when the
+Create a custom [sandbox policy](/how-it-works/policies/overview) when the
 agent needs more filesystem access, package registries, source hosts, tool
 servers, or other destinations.
 
@@ -61,14 +56,48 @@ provider, and pass the agent command after `--`:
 ```shell
 openshell sandbox create \
   --name my-agent \
-  --from agent:local \
-  --provider claude-code \
-  -- claude
+  --from ghcr.io/anomalyco/opencode:latest \
+  --provider openrouter \
+  -- opencode -m openrouter/nvidia/nemotron-3.5-lightning:free
+```
+
+OpenCode detects the OpenRouter credential and starts with the model passed to
+`-m`. This example uses a free model, so it works without OpenRouter credits.
+Choose any model from `opencode models openrouter`.
+
+For more control over what the agent can access, refer to
+[Policies](/how-it-works/policies/overview).
+
+**4. Grant more access as the agent needs it.**
+
+When the agent reaches a destination that policy does not allow, OpenShell
+denies the request and drafts a rule for it. The
+[policy advisor](/how-it-works/policies/advisor)'s mechanistic mapper groups
+recent denials by host, port, and calling program, then submits a narrow
+proposal to the gateway. The gateway checks each proposal with the
+[policy prover](/how-it-works/policies/prover) before you review it.
+
+List pending proposals from the host:
+
+```shell
+openshell rule get my-agent --status pending
+```
+
+Approve a proposal when its rule matches the access you intend to grant, or
+reject it with a reason:
+
+```shell
+openshell rule approve my-agent --chunk-id <chunk-id>
+
+openshell rule reject my-agent \
+  --chunk-id <chunk-id> \
+  --reason "Not needed for this task."
 ```
 
-Add `--policy sandbox-policy.yaml` when the workload needs a custom policy. The
-command after `--` becomes the sandbox's main process, and every child process
-it starts remains inside the sandbox boundary.
+Approved rules hot-reload into the running sandbox without a restart, so the
+agent can retry the request. To let the agent propose its own narrower rules,
+or to approve proposals automatically when the prover finds no new risk, refer
+to [Policy Advisor](/how-it-works/policies/advisor).
 
 ## Examples
 
 
@@ -83,7 +83,7 @@ client = OpenAI(
 )
 
 response = client.responses.create(
-    model="nvidia/nemotron-3-nano-30b-a3b",
+    model="nvidia/nemotron-3-super-120b-a12b",
     input="Hello!",
 )
 print(response.output_text)
@@ -103,24 +103,26 @@ starting templates you copy and adapt, not as defaults.
 ## Attach a Provider to a Running Sandbox
 
 ```shell
-openshell sandbox provider attach inference-demo nvidia-prod
+openshell sandbox provider attach inference-demo nvidia-prod --wait
 openshell sandbox provider list inference-demo
 ```
 
-Running sandboxes poll for provider and effective-policy changes. Launch a new
-process after attachment so it receives the new credential placeholder:
+Running sandboxes poll for provider and effective-policy changes. `--wait`
+confirms the sandbox has applied the attachment. Launch a new process so it
+receives the new credential placeholder:
 
 ```shell
-openshell sandbox exec inference-demo -- python app.py
+openshell sandbox exec --name inference-demo -- python app.py
 ```
 
 An already-running process does not gain new environment variables. Credential
-rotation and detach still take effect immediately at placeholder resolution.
+rotation and detach take effect once the sandbox applies the provider change.
+Use `--wait` to confirm that change before relying on it.
 
 Detach the provider to revoke its policy and credential access:
 
 ```shell
-openshell sandbox provider detach inference-demo nvidia-prod
+openshell sandbox provider detach inference-demo nvidia-prod --wait
 ```
 
 ## Use a Custom or Self-hosted Endpoint
@@ -238,7 +240,7 @@ Earlier releases configured one shared route:
 openshell provider create --name nvidia-prod --type nvidia --from-existing
 openshell inference set \
   --provider nvidia-prod \
-  --model nvidia/nemotron-3-nano-30b-a3b \
+  --model nvidia/nemotron-3-super-120b-a12b \
   --timeout 300
 ```
 
@@ -259,7 +261,7 @@ openshell provider create \
   --name nvidia-native-prod \
   --type nvidia-native \
   --from-existing
-openshell sandbox provider attach inference-demo nvidia-native-prod
+openshell sandbox provider attach inference-demo nvidia-native-prod --wait
 ```
 
 OpenShell does not export stored credential values or change a provider's
 
@@ -164,6 +164,10 @@ The metadata emulator serves tokens with the `cloud-platform` OAuth2 scope,
 which grants access to any GCP API the underlying service account has IAM
 permissions for. Add the target API hosts to your sandbox network policy:
 
+Attach `my-gcp` to the sandbox first. Because the `google-cloud` profile has no
+endpoints, each API endpoint must bind to that provider instance. Without the
+binding, OpenShell withholds its access token from the sandbox.
+
 ```yaml
 network_policies:
   gcp_apis:
@@ -174,23 +178,22 @@ network_policies:
         protocol: rest
         access: read-write
         enforcement: enforce
+        credential_binding:
+          provider: my-gcp
     binaries:
       - { path: /usr/bin/curl }
       - { path: /usr/bin/node }
       - { path: "/sandbox/.uv/python/**" }
       - { path: "/sandbox/.venv/**" }
 ```
 
-Or update a live sandbox directly:
+For a running sandbox, export its base policy. Remove the metadata header above
+the `---` line, add the endpoint and binaries shown above, then apply the file:
 
 ```shell
-openshell policy update my-sandbox \
-  --add-endpoint "*.googleapis.com:443:read-write:rest:enforce" \
-  --binary "/usr/bin/curl" \
-  --binary "/usr/bin/node" \
-  --binary "/sandbox/.uv/python/**" \
-  --binary "/sandbox/.venv/**" \
-  --wait
+openshell policy get my-sandbox --base > sandbox-policy.yaml
+# Edit sandbox-policy.yaml to add the gcp_apis rule shown above.
+openshell policy set my-sandbox --policy sandbox-policy.yaml --wait
 ```
 
 ## Network Policy
 
@@ -891,10 +891,11 @@ Each attached provider with a matching profile contributes a provider policy lay
 
 Updating a custom provider profile affects every provider instance whose `type` matches that profile ID. Provider instances are not rewritten, and sandbox-authored policies are not modified. Running sandboxes observe the updated provider-derived policy on their next config sync. If a gateway-global policy is active, provider-derived policy layers remain suppressed.
 
-The CLI can infer a provider profile from a recognized sandbox command and
-auto-create the provider from profile discovery. Attach a different existing
-provider explicitly with `--provider`, or use `openshell sandbox provider
-attach` after creation.
+Name a provider with `--provider` when creating a sandbox. If no provider has
+that name and it matches an imported profile ID, the CLI can create the
+provider from local profile discovery. The trailing sandbox command does not
+select a provider. Use `openshell sandbox provider attach` to add an existing
+provider after creation.
 
 List providers attached to a sandbox:
Original file line number	Diff line number	Diff line change
`@@ -6302,6 +6302,7 @@ mod tests {`
`6302`	`6302`	`"google-vertex-ai",`
`6303`	`6303`	`"nvidia",`
`6304`	`6304`	`"openai",`
	`6305`	`+ "openrouter",`
`6305`	`6306`	`"pypi"`
`6306`	`6307`	`]`
`6307`	`6308`	`);`