OpenShell Policy Prover

Umbrella issue for the OpenShell Policy Prover (OPP) roadmap.

OPP uses Z3 SMT solving to formally verify that sandbox policies enforce what the author intended. The base Rust implementation landed in #741 and includes binary capability modeling, GitHub credential scopes, exfiltration path detection, write-bypass analysis, and the native openshell policy prove CLI.

Foundation (merged)

• 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

• Deny-rule support in prover modeling (NVIDIA/OpenShell#1061)
• SaaS connector permission modeling: Slack, Discord, Telegram
• MCP tool permission modeling: L4/L7 binary + MCP tool semantics
• Cross-sandbox / multi-agent reasoning: verify flows across connected sandboxes
• Policy Advisor integration: validate policy proposals before approval (NVIDIA/OpenShell#1038, NVIDIA/OpenShell#1062)
• CI gate: run OPP against example policies in CI

Current Status

The prover foundation is merged. This roadmap item remains open for expansion and integration work, especially Policy Advisor proposal validation and richer policy modeling.

Start with the merged base implementation in issue #741 and the native openshell policy prove CLI. Choose one expansion area, such as deny-rule support in #1061 or Policy Advisor validation in #1038 and #1062, then define its scope with the maintainers. Done means the selected policy-modeling or integration work is implemented and validated against the relevant example policies or proposals.