> proving the guardrail ran is weaker than proving the model had no unsafe branch left out.
that’s the crack in the whole pitch, and it’s not a small one. a zk proof that some judge approved a tool call only tells you the wrapper behaved, not that the policy was complete or that the agent couldn’t route around it with a missing branch, stale contract, or just a dumbly permissive intent spec.
so the paper is mostly selling verifiable enforcement of a classifier, not verifiable safety of the agent. useful maybe, but calling that a cryptographic guardrail is doing a lot of marketing work.
> Proving the guardrail ran is weaker than proving the model had no unsafe branch left out.
I’d call that the wrong comparison. If the host is untrusted, “the guardrail ran” is the part you can actually audit, while “no unsafe branch was left out” is just a bigger model assurance problem wearing cryptography as a hat.