I've been reading a lot of pieces this year about how AI agents get authorized: which protocol issues the token, which framework signs the card, and which policy engine checks the scope. Almost none of them ask the question that actually matters once an agent is running in production. If you write a policy that says an agent can read customer records but never delete them, how do you actually know that's true? Testing tells you the policy holds for every case someone thought to write a test for. It says nothing about the cases nobody thought of. That gap is exactly what formal verification is built to close, and over the past few months it has quietly moved out of academic papers and into tools people are shipping right now.

Testing Only Tells You What You Checked

Most agent authorization today gets validated the way most software gets validated: write a policy, write some tests, watch the tests pass, ship it. That works fine when the input space is small and predictable. Agent input isn't either. An agent authorization policy has to hold across an effectively unbounded set of natural language requests, tool combinations, and execution contexts, and a test suite only covers the paths someone remembered to write down.

Google's own engineering team put this plainly when they announced a new verification framework in August. They pointed out that unit tests can miss the infinite set of possible inputs that show up in production, and that a policy overfit to its test suite can fail badly the moment it meets a case nobody anticipated. Their answer combines the usual heuristic testing with actual mathematical proof that the policy behaves correctly across its full input space.

Formal Verification Just Left the Whitepaper

Two real examples show this shift isn't theoretical anymore. Google shipped a formal verification framework for CEL, the Common Expression Language that sits underneath a lot of production policy engines, this month. It pairs testing with mathematical proofs that a policy behaves correctly across its full input space, not just the inputs someone happened to test.

AWS built something similar earlier, though quieter about it. Cedar, the policy language AWS uses for runtime authorization, has a parallel verification effort behind it built in Lean and Rust, checking that the policy engine itself behaves the way its specification claims. That's a meaningfully different guarantee than testing. A test tells you the engine passed the cases you tried. A Lean proof tells you the engine can't misbehave in a way the proof would have caught, for any input.

Neither of these fully solves agent authorization on its own. They verify the policy engine and the policy language. They don't yet verify that a specific agent, given a specific natural language instruction, will only ever generate actions the policy actually permits. That's the harder problem, and it's where the research is heading next.

A July 2026 paper takes a direct run at that harder problem. It formalizes agent authorization as what the authors call a cryptographically verifiable relation, binding together the specific agent, the specific request it made, the execution context it made it in, and whether that combination actually satisfies the policy. The goal is cryptographic evidence that a real request, from a real agent, in a real context, actually complied with policy, not merely a policy document that reads correctly on paper.

A separate paper goes after a narrower but related target, agent skills specifically. It proposes a three-layer approach toward what the authors call a mechanically checkable capability-containment proof, essentially a machine-checked guarantee that a given agent skill can't reach outside the boundaries it was granted. The paper's own reference list cites Cedar directly as a formally verified policy language paired with that same Lean and Rust verification effort, which says something about how small and interconnected this research space still is.

Why Translation Is the Real Bottleneck Here

Here's the part that made me rethink how close any of this actually is to production-ready. All of the proof techniques above assume you already have a precise, formal policy to verify against. Agents don't start there. They start with a natural language instruction, a system prompt, a task description written by a person who was not thinking in formal logic when they wrote it.

One recent paper names this gap directly and tries to build a bridge across it. It calls its approach the "Verification Sandwich", a layered pipeline that takes natural language agent instructions and automatically translates them into a formal policy language, specifically Cedar. A policy engine can then enforce that policy, and a proof can then check it. If I were evaluating any of this for production use, the translation step is the part I'd bet against first. Getting a proof right is hard but well understood. Getting that translation right every time is the part still genuinely unsolved, especially for instructions nobody wrote with formal verification in mind.

A related project, Lean4Agent, takes a different angle on a similar problem, formally modeling and verifying an agent's actual workflow and execution trajectory rather than just its authorization boundary. It's a reminder that authorization is only one piece of what people are trying to formally verify about agents right now. Behavior, trajectories, and tool use are all getting the same treatment in parallel.

What This Means in Practice

A few things follow from where this research actually stands if you're building or evaluating agent authorization today.

Don't confuse a well-tested policy with a proven one. They're different guarantees, and the industry examples above show real companies now building policies that carry both kinds of evidence.

Watch the policy language you standardize on. Cedar and CEL both have serious verification work behind them now. A policy language with no formal backing behind it is a weaker long-term bet, even if it's the more familiar choice today.

Treat the natural-language-to-policy translation step as the actual risk surface. If an agent's permissions get generated automatically from a prompt or instruction set, that step is the most likely place for a gap to open up between what you meant and what actually got formally verified.

Conclusion

Authorization protocols answer which agent can act. Formal verification research is starting to answer whether a given policy can be proven correct rather than just tested. Neither one alone guarantees an agent stays inside its boundaries in production, but the tools shipping this year are closer to that guarantee than anything available twelve months ago.

The translation step is where the bottleneck actually sits right now, and it's the piece of this stack that still has the least maturity behind it. If your agents are making decisions you'd have to explain to an auditor, that gap deserves close attention.