--- title: "Google introduces formal verification for CEL policies with Z3" description: "The August 18 framework targets logical errors in expressions and policies. Defining the property to prove and understanding the model’s boundaries remain essential." url: https://kurddevelopers.com/en/news/google-cel-formal-verification-z3-policy-checking-august-2026 language: en # English type: news published: 2026-08-18T20:00:00.000Z updated: 2026-11-03T17:05:12.000Z author: "Osamah Ismail" author_url: https://kurddevelopers.com/en/author/1 section: "Programming" tags: ["Google","CEL","Programming","Formal Verification"] sources: ["Google Open Source Blog — 18 August 2026: https://opensource.googleblog.com/2026/08/securing-the-agentic-era-introducing-formal-verification-for-cel.html","CEL — language overview: https://cel.dev/"] image: https://kurddevelopers.com/uploads/2026/11/cel-fullcolor-rgb-notype-78e19fe4.png translations: ku: https://kurddevelopers.com/news/google-cel-formal-verification-z3-policy-checking-august-2026 ar: https://kurddevelopers.com/ar/news/google-cel-formal-verification-z3-policy-checking-august-2026 publisher: Kurd Developers publisher_url: https://kurddevelopers.com/ --- # Google introduces formal verification for CEL policies with Z3 > The August 18 framework targets logical errors in expressions and policies. Defining the property to prove and understanding the model’s boundaries remain essential. ![Official Common Expression Language identifying artwork. Image: Google.](https://kurddevelopers.com/uploads/2026/11/cel-fullcolor-rgb-notype-78e19fe4.png) Google announced the CEL Formal Verification Framework on August 18, 2026. It uses Z3 to examine defined properties of CEL expressions and policies, including equivalence and security invariants. CEL is an expression language embedded in applications. Its uses include API filters, validation constraints and authorisation rules. ## How is this different from testing? A test examines behaviour for particular inputs. Formal verification seeks to establish a property within a defined model. Specifying that property remains an important engineering task. The distinction matters for access policies because a small change in grouping can alter who is admitted. A shorter expression does not automatically preserve the original behaviour. Passing familiar examples also cannot, by itself, answer every question relevant to the policy. A reviewer needs to understand the intended requirement before deciding whether a rewrite maintains it. ## An independent logical example Suppose access requires membership together with either a paid subscription or a trial. One expression is: `member && (paid || trial)` The expression `(member && paid) || trial` would instead accept a non-member when `trial=true`. Membership has changed from a requirement applying to both alternatives into one applying only to the first branch. This is an illustration we wrote to explain the logic, rather than a result from running the verifier. It shows why expressions can look similar while producing different decisions. The review question is whether behaviour matches the intended policy. Brevity and readability are useful, but neither establishes equivalence on its own. ## An inconclusive result is not a proof The announcement explains that an issue depending on an unmapped custom function can produce an `Inconclusive` result. That means the analysis has not reached a complete determination; it should not be read as confirmation of correctness. For teams using AI to rewrite policies, a useful starting point is to define the conditions that must survive the change. The modified policy can then be examined against those same conditions. Our assessment is that testing and formal verification can provide complementary evidence. A proof of a defined property needs to be interpreted within that scope, rather than expanded into a blanket guarantee about an entire application. This keeps the engineering objective clear: identify what must remain true, make the assumptions visible and evaluate the change against an explicit requirement. ## Sources - [Google Open Source Blog — 18 August 2026](https://opensource.googleblog.com/2026/08/securing-the-agentic-era-introducing-formal-verification-for-cel.html) - [CEL — language overview](https://cel.dev/) **Sources:** Google Open Source Blog — 18 August 2026: https://opensource.googleblog.com/2026/08/securing-the-agentic-era-introducing-formal-verification-for-cel.html, CEL — language overview: https://cel.dev/ --- Published by [Kurd Developers](https://kurddevelopers.com/) on 2026-08-18. Cite as: “Google introduces formal verification for CEL policies with Z3”, Kurd Developers, https://kurddevelopers.com/en/news/google-cel-formal-verification-z3-policy-checking-august-2026