--- title: "Securing the agentic era: Introducing formal verification for CEL" url: https://daily.dev/posts/securing-the-agentic-era-introducing-formal-verification-for-cel-fpythtftu source_url: http://opensource.googleblog.com/2026/08/securing-the-agentic-era-introducing-formal-verification-for-cel.html type: article source: "Google Open Source Blog" published: 2026-08-18T20:49:47.073Z updated: 2026-08-18T20:50:10.966Z tags: ["ai-agents", "policy-as-code"] reading_time: 5 upvotes: 1 comments: 0 language: en --- > ## Documentation Index > Fetch the complete documentation index at: https://daily.dev/llms.txt > Use this file to discover all available pages before exploring further. # Securing the agentic era: Introducing formal verification for CEL **[Google Open Source Blog](https://daily.dev/sources/googleoss)** · 5 min read · 1 upvotes · 0 comments ## Summary Google's Common Expression Language (CEL) now has a Formal Verification Framework powered by the Z3 theorem prover, letting developers mathematically prove the correctness and security of CEL expressions and policies. It targets the risk of AI agents autonomously authoring or refactoring policies where unit tests can't cover every possible input. The framework supports equivalence checks (verifying refactors preserve behavior), validity checks (proving a condition holds for all inputs), and invariant checks on CEL policies using assume/assert blocks, with examples showing how it catches operator-precedence bugs, incomplete port-range guardrails, and privilege-escalation flaws. It uses three-pass taint tracking to avoid false positives and bounded-model checking to control verification cost, and is available now via a REPL and GitHub repo for integration into CI/CD pipelines. ## Full article daily.dev links to this article rather than hosting it. Read it at the original source: ## Questions this post answers ### What is the CEL Formal Verification Framework and how does it work? It is a new tool from the CEL project that uses the Z3 theorem prover to mathematically prove properties of CEL expressions and policies, rather than relying only on unit tests. It supports equivalence checks between two expressions, validity checks that hold across all inputs, and invariant checks on CEL policy files using assume and assert blocks, exhaustively searching the input space for counterexamples. _Teams adopting AI-generated policy code can track tooling like this CEL verifier on daily.dev._ ### How does the CEL verifier avoid false positives from unmapped custom functions? It uses three-pass taint tracking: when a potential issue depends on a custom function or external variable the solver doesn't fully understand, the verifier isolates and marks that result as Inconclusive instead of reporting it as a Violation. This guarantees that every reported Violation is a reproducible, real bug, preventing noisy false alarms from breaking a CI pipeline. _Engineers wiring policy checks into CI can follow verification tooling updates on daily.dev._ ### How can I prove a refactored CEL boolean expression is equivalent to the original? Using the CEL verifier's REPL, write an equiv statement comparing the two expressions with the <=> operator; the tool exhaustively checks all inputs and reports Verified or Violated with a counterexample. For example, rewriting (is_prod && port==80) || (is_prod && port==443) without correct parentheses as is_prod && port==80 || port==443 gets flagged Violated because it wrongly allows port 443 outside production. _Developers refactoring policy logic with AI agents can watch for verification tools like this on daily.dev._ ## Similar posts on daily.dev - [When AI Writes the World’s Software, Who Verifies It?](https://daily.dev/posts/when-ai-writes-the-world-s-software-who-verifies-it--tsppkfj9s) · Hacker News · 1 upvotes · 0 comments - [Claude Can \(Sometimes\) Prove It](https://daily.dev/posts/claude-can-sometimes-prove-it-wshuhsu5p) · Hacker News · 2 upvotes · 0 comments - [Prediction: AI will make formal verification go mainstream — Martin Kleppmann’s blog](https://daily.dev/posts/prediction-ai-will-make-formal-verification-go-mainstream-martin-kleppmann-s-blog-j1btzfnpe) · Lobsters · 2 upvotes · 0 comments --- Tags: [#ai-agents](https://daily.dev/tags/ai-agents), [#policy-as-code](https://daily.dev/tags/policy-as-code) [View this post on daily.dev](https://daily.dev/posts/securing-the-agentic-era-introducing-formal-verification-for-cel-fpythtftu)