feat(prover): OpenShell Policy Prover (OPP) roadmap

[zredlined]

Problem Statement

The OpenShell Policy Prover (OPP) uses Z3 SMT solving to formally verify that sandbox policies enforce what the author intended. The base implementation (issue #699, PR #741) covers binary capability modeling, GitHub credential scopes, exfiltration path detection, and write-bypass analysis.

OPP is not yet tracked on the roadmap. This issue serves as the umbrella for OPP post-merge work and expansion.

Roadmap

Foundation (in progress)

• Rust-native prover with Z3 solver (feat: Add formal policy verification (OpenShell Policy Prover) to Python SDK #699, PR feat(prover): add native Rust policy prover with Z3 solver #741)
• Binary capability registry (git, curl, node, python3, claude, etc.)
• GitHub API and credential scope modeling
• Exfiltration and write-bypass verification queries
• CLI: openshell policy prove

Expansion

• SaaS connector permission modeling — Slack, Discord, Telegram (see child issue)
• MCP tool permission modeling — L4/L7 binary + MCP tool semantics (see child issue)
• Cross-sandbox / multi-agent reasoning — verify flows across connected sandboxes (see child issue)
• Policy Advisor integration — validate proposals before approval
• CI gate — run OPP against example policies in CI

Context

OPP is scoped to the sandbox trust boundary. It validates policy intent vs actual effect given binaries, endpoints, and credentials. It does not attempt to prove full deployment architecture, host-side components, or operational state.

Related: #699, PR #741

[zredlined]

Moved to Linear for roadmap tracking.