I built OpenShell's Z3 policy prover and ran 29 checks. It caught everything except the metadata address.

NVIDIA OpenShell's standalone prover formally checks agent policies against a boundary. I built it from source (Z3 via a pip wheel) and ran 29 candidate/boundary pairs: REST escalation, L4 laundering and new binaries all caught with concrete counterexamples — but a policy whose only rule is curl to 169.254.169.254 passes even an empty boundary, because loopback and link-local are carved out of the model in ip.rs (HARD_V4).