# Securing the agentic era: Introducing formal verification for CEL

DevFeed: [Securing the agentic era: Introducing formal verification for CEL](<https://devfeed.tech/articles/securing-the-agentic-era-introducing-formal-verification-for-cel-34318.md>)

Original publisher: [Read original article](<http://opensource.googleblog.com/2026/08/securing-the-agentic-era-introducing-formal-verification-for-cel.html>)

Author: Google Open Source (noreply@blogger.com)

Published: 2026-08-18T18:30:00Z

Content type: release

Language: en

Sources: [Google Open Source Blog](<https://devfeed.tech/sources/google-open-source-blog.md>)

Topics: [Formal verification](<https://devfeed.tech/topics/formal-verification.md>), [Automated reasoning](<https://devfeed.tech/topics/automated-reasoning.md>), [Testing](<https://devfeed.tech/topics/testing.md>), [Artificial Intelligence](<https://devfeed.tech/topics/ai.md>)

Tags: [agent](<https://devfeed.tech/tags/agent.md>), [ai](<https://devfeed.tech/tags/ai.md>), [ai-agent](<https://devfeed.tech/tags/ai-agent.md>), [automated-reasoning](<https://devfeed.tech/tags/automated-reasoning.md>), [cel](<https://devfeed.tech/tags/cel.md>), [common-expression-language](<https://devfeed.tech/tags/common-expression-language.md>), [formal-verification](<https://devfeed.tech/tags/formal-verification.md>), [open-source](<https://devfeed.tech/tags/open-source.md>), [security](<https://devfeed.tech/tags/security.md>), [testing](<https://devfeed.tech/tags/testing.md>), [verification](<https://devfeed.tech/tags/verification.md>), [z3](<https://devfeed.tech/tags/z3.md>)

## AI overview

Google's Common Expression Language (CEL) Formal Verification Framework is available for proving the correctness of CEL expressions and policies. Powered by the Z3 theorem prover, it complements heuristic testing by using mathematical proofs to identify logic flaws, equivalence issues, and potentially unsafe policy behavior.

## Source excerpt

by Sean Huh, Common Expression Language Team We are rapidly entering an era where AI agents can autonomously draft, refactor, and deploy policies that protect our users and our systems. But this velocity introduces a vital question: How do we trust AI-generated policies? Unit tests may fail to cover the infinite set of possible inputs that occur in production; thus, an AI agent that overfits its policy to existing tests may fail spectacularly in production. To secure automated policy authoring, we must combine heuristic testing with mathematical proofs. We are thrilled to announce the Common Expression Language (CEL) Formal Verification Framework is now available. Powered by the Z3 theorem prover, this framework allows you to prove the correctness of your CEL expressions and policies, serving as the ultimate safety net for the agentic policy. Automated reasoning definitively answers questions like: "Is there any combination of inputs that allows an unapproved request into production?" "Are we absolutely certain this AI-refactored policy matches the original behavior?" "Can a bad actor manipulate this rule to force an evaluation error?" Formal verification establishes mathematical certainty across the infinite spectrum of inputs. Proven policies protect your users and system while giving auditors clear proof of compliance. To see these capabilities in action, watch our video demonstrating how the CEL Verifier REPL catches subtle logic flaws in seconds: Proving rules from the ground up Getting started with formal verification doesn't require learning complex architectures right away. You can evaluate simple standalone CEL expressions to catch edge cases that tests easily miss. (Note: The examples below use our interactive REPL syntax--check out the REPL documentation to follow along!) 1. Catching logic bugs in simple expressions (Equivalence) How do you guarantee a refactored rule behaves identically to the original? Suppose we have a policy that allows ports 80 or 443