OpenShell Policy Prover

[linear]

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 is in review (GitHub #699, PR #741) and covers binary capability modeling, GitHub credential scopes, exfiltration path detection, and write-bypass analysis.

Foundation (in progress)

• 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
• MCP tool permission modeling — L4/L7 binary + MCP tool semantics
• Cross-sandbox / multi-agent reasoning — verify flows across connected sandboxes
• Policy Advisor integration — validate proposals before approval
• CI gate — run OPP against example policies in CI

[cgwalters]

So...I was rather surprised when I was building openshell (having not provided the bundled-z3 as a feature) and I realized that this project was including a SMT solver. I had to know why that is...and right now my impression is that openshell prove is pretty experimental.

There's a bit of a clash to me here in choosing YAML to define policies (a data serialization structure for which I think the general internet trend is against (ref e.g. https://noyaml.com and https://kubernetes.io/docs/reference/encodings/kyaml/ and https://blog.yossarian.net/2025/09/22/dear-github-no-yaml-anchors etc) and then bolting a SMT solver onto it. There's...some other possible choices in this space. (TOML is obviously a lot simpler, but far from the only choice...in some corners of the internet there's a resurgence in mini-languages (like go.mod)).

But another choice might be https://nickel-lang.org/ which I admit to not having real world experience with, but I like a lot of what I read.

Anyways, one other thought here is that while validating the L7 proxy stuff is kind of useful, what I think is much more important is tooling to validate compositions of agents - because I think a lot of real world security can be gained by having truly distinct agents (sandboxes) with their own limited capabilities that communicate in structured ways. I'd love to see OpenShell perhaps having some opinion on that problem domain.

But anyways honestly I feel this prover stuff is just too half baked as is right now to be a default-compiled feature.