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 in production. An agent might factor the is_prod check like so:
equiv
(is_prod && port == 80) || (is_prod && port == 443)
<=>
is_prod && port == 80 || port == 443Because logical AND has a higher operator precedence than OR, the verifier immediately flags Violated, and outputs the exact exploit: in a non-production environment (is_prod = false), the rule mistakenly allows port 443. Fixing the grouping parentheses returns Verified.
2. Enforcing exhaustive guardrails (Validity)
This capability scales directly to use cases like Kubernetes Validating Admission Policies. Suppose an engineer writes a guardrail expression that assumes every request will either be on a low port (under 80) or a high port (over 1024):
valid request.port > 1024 || request.port <= 80When we check validity (whether an expression holds true for all inputs), the verifier exhaustively searches the entire integer space, flags Violated, and outputs the exact counterexample:
[VIOLATED] Condition is not always true. Counterexample input:
request.port = 813. Guaranteeing security invariants with CEL Policy
While the verifier works perfectly with standalone CEL expressions, complex environments compose multiple rules and variables. Here, the CEL policy format shines. Using assume and assert blocks, the verifier proves a mathematical implication: if the assumptions hold, the assertions must also hold.
name: workload_admission
rule:
variables:
- is_admin: 'request.auth.claims.groups.exists(g, g == "admin")'
match:
# A subtle flaw introduced during authoring:
- condition: 'request.is_privileged && request.is_prod'
output: 'true'
- condition: 'variables.is_admin || request.has_approval'
output: 'true'
- output: 'false'
verification:
invariants:
- id: universal_no_unapproved_privileged_prod
assume:
- 'request.has_approval == false'
- 'variables.is_admin == false'
assert:
- 'rule.result == false'The first condition admits privileged workloads into production without checking for approval or admin status. The verifier flags this and provides an example that exploits the issue:
Invariant 'universal_no_unapproved_privileged_prod' violation detected. Counterexample input:
request.is_privileged = true
request.is_prod = true
request.has_approval = false
request.auth.claims.groups = []Assertions and assumptions define the boundaries of acceptable agent behavior, allowing developers to configure CI/CD pipelines to validate AI-generated changes simply and securely.
Under the hood: High-fidelity mathematical modeling
Translating a dynamic language into the Satisfiability Modulo Theories (SMT) domain requires immense engineering rigor to prevent the solver from hanging or hallucinating bugs. Our engine provides:
Zero false positives via three-pass taint tracking
Traditional verification tools are prone to “solver hallucinations”—reporting fake bugs when encountering custom domain-specific functions or external variables they don’t fully understand. To eliminate this noise, if a potential issue relies on an unmapped custom function, the verifier isolates and flags it as Inconclusive rather than breaking your CI pipeline with a false alarm. This guarantees every Violation report is a 100% real, reproducible bug.
Deep structural extensionality
The Formal Verification Framework offers configurable-depth bounded-model checking to prevent infinite loops within SMT quantifiers. These configurable limits allow you to control the cost of verification when analyzing deep structure equivalence in expressions like [[1], [2]] == [[1], [2]].
The mandatory bridge of trust
In the agentic era, code writes code. Mathematical proof isn’t just a nice-to-have; it is the fundamental bridge of trust developers require to let AI operate autonomously in their most sensitive systems. Get started with the CEL Formal Verification Framework, to take the next step toward a more secure agentic future today!
Let us know what you think—issues, pull requests, and feedback are always welcome!
