feat(prover): add native Rust policy prover with Z3 solver

[zredlined]

Summary

Native Rust implementation of the OpenShell Policy Prover (OPP) using Z3 SMT solving. Answers two questions about any sandbox policy:

1. Can data leave this sandbox? — finds exfiltration paths through uninspected (L4-only) endpoints and wire protocol bypasses
2. Can the agent write despite read-only intent? — finds write operations that bypass read-only policy through binary capabilities and credential scopes

openshell policy prove is now a native CLI command — no Python, no subprocess, no PYTHONPATH.

Supersedes #703 (Python prototype). Closes #699.

Related Issue

Closes #699

Changes

New crate: crates/openshell-prover/

• model.rs — Z3 constraint model encoding policy rules, binary capabilities, and credential scopes as boolean satisfiability constraints
• queries.rs — two verification queries (exfiltration, write bypass)
• policy.rs — policy YAML parser with intent detection, L7 enforcement helpers, workdir modeling
• registry.rs — binary capability registry (git, curl, node, claude, etc.) embedded at compile time via include_dir!
• credentials.rs — credential and API capability loading
• accepted_risks.rs — risk acceptance matching by query + host
• report.rs — terminal and compact (CI) output
• finding.rs — finding types and risk levels (HIGH, CRITICAL only)
• lib.rs — public prove() API + 7 tests

Registry data (crates/openshell-prover/registry/):

• 9 binary capability descriptors, 1 API descriptor (GitHub)
• Embedded into the binary at compile time; --registry CLI flag overrides with a filesystem path for custom registries

CLI integration (crates/openshell-cli/src/main.rs):

• openshell policy prove calls openshell_prover::prove() directly

Dependencies (Cargo.toml):

• z3 = "0.19" — links against system libz3 via pkg-config
• include_dir = "0.7" — compile-time registry embedding
• glob = "0.3" — replaces hand-rolled glob matching

Build: system Z3 vs bundled

CI uses system libz3-dev (pre-installed in the CI image) so Z3 never compiles from source. sccache only wraps rustc — not the cmake C++ build z3-sys runs — so the bundled feature caused ~30 min CI builds on every cache miss. With the system library, Z3 link time is always zero.

Local development: install Z3 via brew install z3 (macOS) or apt install libz3-dev (Linux). For environments without system Z3, an opt-in feature compiles from source:

cargo build -p openshell-prover --features bundled-z3

Review feedback addressed:

• Port types changed from u32 to u16 to match runtime validation (prevents silently accepting >65535)
• include_workdir serde default changed from true to false to match runtime behavior (openshell-policy uses #[serde(default)])
• Registry loading switched from fragile CARGO_MANIFEST_DIR/CWD filesystem paths to compile-time embedding
• Hand-rolled glob matching replaced with glob crate
• Removed unused deps: openshell-policy, openshell-core, thiserror, tracing

Testing

• cargo test -p openshell-prover --features bundled-z3 — 7/7 tests pass
• cargo check -p openshell-cli --features openshell-prover/bundled-z3 — CLI compiles
• End-to-end: openshell policy prove --compact detects exfil + write bypass on test fixture

Checklist

• Follows Conventional Commits
• Commits are signed off (DCO)
• SPDX license headers on all new files
• Z3 prerequisite documented in CONTRIBUTING.md

[zredlined]

@NVIDIA/openshell-codeowners The Rust checks for PR #741 are failing because z3-sys needs libclang for bindgen, and our ghcr.io/nvidia/openshell/ci:latest image doesn’t include it. I can patch branch-checks.yml to install clang/libclang-dev in the Rust jobs for an immediate unblock, but I think we should also update deploy/docker/Dockerfile.ci and republish the CI image as the proper fix. Do folks prefer the workflow-level unblock first, or do we want to fix the CI image before rerunning checks?

[johntmyers]

@NVIDIA/openshell-codeowners The Rust checks for PR #741 are failing because z3-sys needs libclang for bindgen, and our ghcr.io/nvidia/openshell/ci:latest image doesn’t include it. I can patch branch-checks.yml to install clang/libclang-dev in the Rust jobs for an immediate unblock, but I think we should also update deploy/docker/Dockerfile.ci and republish the CI image as the proper fix. Do folks prefer the workflow-level unblock first, or do we want to fix the CI image before rerunning checks?

I'd make sure it's in the image.

[mjamiv]

We run 4 OpenClaw AI agent sandboxes on a single OpenShell host, each with its own network policy (~24 endpoints, post-Phase 1 security hardening). Right now we audit for exfiltration paths manually — cross-referencing L4-only endpoints, binary capability sets, and credential scopes across four policy files is tedious and error-prone.

A native openshell policy prove command is exactly what's missing from our workflow. The two query model (exfil path + write bypass) maps directly onto the two threat classes we care most about: data leaving a sandbox through an uninspected tunnel, and an agent acquiring write access beyond its intended scope. Being able to run this in CI on every policy change would close the gap cleanly.

We'd be happy to be early testers once it ships — our policy set is a reasonable real-world fixture (multiple sandboxes, shared host, per-agent binary allowlists, split REST/WebSocket policies). Happy to share sanitized policy YAML if it's useful for the registry or test corpus.