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.

Sit with the shape of that bug for a second. The refactor is shorter than what it replaced. It removes a duplicated clause. It's the change a careful engineer would make and a reviewer would approve, and approving it 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. Neither is an interaction between two policy files that are individually correct. Neither is 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 holds up well against sloppy agents and badly against subtle ones. That's an uncomfortable place to be, because the agents keep getting less sloppy.

What proving a policy actually 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 questions that testing can't answer. Not "does this pass my cases" but "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.

That's the artifact worth wanting. A specific request that defeats your policy, which you can paste into a test, rather than a warning you have to go interpret.

The feature that makes it usable

Verification tools have a reputation among engineers who've had to run them, and it's earned. 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.

I'd argue that's the part to pay attention to, more than the proving. A verifier that reports what it can't determine is one you can wire into CI and let block a merge. A verifier that guesses gets an exemption within a month, then gets ignored, then gets removed in a cleanup sprint six months later by someone who notices nobody's looked at 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. That's a real limit and worth naming. Bounded checking means bounded proof.

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 the thing you actually needed was for unapproved privileged workloads 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. They don't delete it.

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. Teams that struggled to write down what their systems should do will struggle to write down what they must never do.

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 answers the question that matters, which is whether the things you approved last quarter actually do what you thought when you approved them.