Can an SMT solver prevent LLM policy drift during agent execution?

Progent secures AI agents by enforcing a "privilege control policy," defined as "a security policy consisting of symbolic rules over tool names and arguments," checked against "every tool call... through a deterministic procedure, enforcing the principle of least privilege." Rules are "allow" or "forbid" entries that can specify "concrete values... wildcards... and regular-expression patterns," and a tool call that "matches no rule" is "blocked by default." In the paper's running example, the policy denies a malicious send_email call that adversarial content injected into the agent's context tries to trigger, and allows a benign send_slack_msg call under the same policy, because the check is "purely symbolic over structured policy rules" and does not depend on the agent's own, manipulable reasoning.

Because "different tasks require different tools and arguments" and "the relevant context evolves at runtime," Progent has an LLM generate the initial policy from the user's task and propose updates as execution proceeds — for instance, after a tool result reveals a TODO requiring more tools, or reveals a specific recipient that narrows a rule to that recipient. Letting an LLM write and revise the policy "introduces non-determinism," so Progent adds a second, deterministic check on top: "each policy update [is] checked by a deterministic SMT solver as either a narrowing (applied automatically) or an expansion (requiring explicit approval)." The paper names the resulting guarantee "monotonic confinement": "the agent's effective action space can only narrow without approval," so that "even if the LLM is manipulated by adversarial inputs" — as when injected email content tries to introduce a new send_email capability — "this deterministic check prevents any silent privilege escalation," while genuine, approved expansions still go through.

The design lands on a split already in the library's Can memory poisoning compromise decision-making even with authorization layers?: a reasoning component can be fooled every time while a separate, non-reasoning check still blocks the resulting action. That paper measures a token-plus-oracle layer at the point of execution without saying how the oracle itself decides; Progent proposes one way to build such an oracle — a symbolic allow/forbid policy plus an SMT-based narrowing/expansion check — and locates its guarantee in the update mechanism, not only in the final per-call check. The two differ in grain: the authorization layer passes or blocks a single step, while Progent's policy is stateful across the run (the paper's P1 through Pi notation), evolving as context accumulates, which moves toward the trajectory-level view in Can step-by-step approval miss harmful behavior patterns? — though Progent's own enforcement is still a call-by-call match against the current policy, not a check over the sequence as a whole.

The excerpt reports the security/utility result only in general terms — Progent "significantly reduces attack success rates while maintaining high utility" on the AgentDojo and ASB benchmarks — without the exact percentages, so the size of that tradeoff is not established here. The paper's own Limitations section is explicit that the guarantee covers silent escalation, not human error in the approval step: "If users incorrectly approve widening updates or give ambiguous initial tasks, Progent may permit policies that exceed minimal privilege." It also scopes the defense to actions: Progent "does not tackle attacks that influence only the agent's textual outputs without triggering dangerous tool calls." Monotonic confinement, then, is a guarantee that privilege cannot expand without a recorded approval, not a guarantee that approval is always given correctly, and not coverage for harm that never passes through a tool call.