Your Agent's Policy Refactor Looked Fine in Review

Here's a policy that allows traffic on ports 80 and 443, but only in production. An agent refactors it to pull the shared condition out front, the way any of us would:

(is_prod && port == 80) || (is_prod && port == 443)

becomes

is_prod && port == 80 || port == 443

That's cleaner. It's also a hole. && binds tighter than ||, so the second expression reads as "production on port 80, or port 443 anywhere," and port 443 is now open in every non-production environment you run. Google's CEL team published that exact example last week alongside a formal verification framework that catches it.

The refactor is shorter than what it replaced and it drops a duplicated clause. It's the change a careful engineer would make and a reviewer would wave through, and waving it through opens a port.

Your approval gate is weaker than you think

Most teams running agents against infrastructure have settled on the same control: the agent proposes, a person approves. We recommend it constantly. It's the right default for the same reason code review is.

But review catches a specific class of problem. A reviewer reads a diff and asks whether it does what it says. That works when the failure is visible in the text, like a dropped condition or a wildcard where a name should be. Operator precedence isn't visible in the text, and an interaction between two policy files that are individually correct doesn't show up there either. Nor does the input nobody thought to imagine, which is what the CEL team means when they write that an agent overfitting a policy to existing tests "may fail spectacularly in production."

So the approval gate catches the sloppy agent and waves the subtle one through. Which is uncomfortable, because they keep getting less sloppy.

What proving a policy looks like

The framework compiles CEL expressions into assertions for Z3, a theorem prover that's been around since long before anyone worried about agentic policy authoring, and asks the question testing can't reach: does any input exist that breaks this.

Ask it whether a guardrail holds for every request, where the engineer assumed traffic is either on a low port or a high one:

valid request.port > 1024 || request.port <= 80

It comes back Violated, with request.port = 81. There's the gap, in the integer space between 80 and 1024, found without anyone guessing that 81 might matter.

The composed case is more interesting, because that's where real policies live. CEL policies let you write assume and assert blocks, and the verifier proves the implication between them: if these things are true, this outcome must follow. Google's example encodes an invariant that unapproved privileged production workloads must be denied, then runs it against a rule whose first condition admits privileged production workloads without checking approval or admin status at all. The verifier returns the counterexample: privileged true, prod true, approval false, group membership empty.

You get a specific request that defeats your policy, in a form you can paste straight into a test.

The feature that makes it usable

Verification tools have an earned reputation among engineers who've had to run them. They cry wolf. A tool that flags twenty things where two are real teaches the team to skim past all twenty, and the two real ones ship.

The CEL engine handles this with three-pass taint tracking. When a potential issue depends on a custom function or an external variable the verifier can't model, it doesn't guess and it doesn't report a violation. It returns Inconclusive. Google's claim is that this makes every Violation report a real, reproducible bug.

That matters more than the proving does. You can wire a verifier into CI and let it block a merge, but only if it admits what it couldn't determine. One that guesses picks up an exemption inside a month, and six months later somebody clearing out dead config deletes it, having noticed nobody read its output since spring. Anyone who has introduced a linter into an unwilling codebase has watched this happen.

The framework also caps how deep it explores inside quantifiers, so it can't hang your pipeline. Worth naming that as the limit it is: what you get back is a proof about the space it was allowed to search.

What this doesn't fix

Verification tells you a policy matches its specification. It has nothing to say about whether the specification was right. If you assert that unapproved privileged workloads must be denied, and what you needed was for them to be denied except during an incident, the prover will happily certify your policy while the wrong rule runs in production. Formal methods move the risk from implementation to intent, and it sits there just as heavily.

This also only applies where policy is expressed in a language a solver can reason about. CEL, Rego, and similar. The moment an agent's real authority lives in a Python script or a set of IAM conditions assembled by string concatenation, you're back to reading diffs.

And there's the obvious constraint: writing invariants is work. Someone has to sit down and articulate what must never happen, in a form precise enough to be mechanically checked. If your team has never managed to write its requirements down, this will not be the document it finally finishes.

What I'd do with this

If you're running agents that touch policy, and you've told yourself the human approval step covers you, go find a policy change an agent made in the last month and check whether a reviewer could have caught a precedence bug in it by reading. My guess is no, for most of them.

Then pick one invariant. The single condition that would embarrass you most if it failed, whatever that is for your systems. Encode it and wire it into the pipeline that merges agent-authored policy changes, then see what it says about the policies you're already running.

That's a smaller commitment than a verification program, and it tells you whether the things you approved last quarter do what you thought they did when you approved them.