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.
Table of contents
Proving rules from the ground upUnder the hood: High-fidelity mathematical modelingThe mandatory bridge of trustQuestions 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.