Implement custom policy invariants verification

Enables policy authors to declare custom logical invariants (`assume` preconditions and `assert` clauses) on `CelPolicy` definitions, mathematically verifying that properties hold across all possible input states.

PiperOrigin-RevId: 915170572

Author: l46kok

README.md

@@ -82,6 +82,8 @@ A policy source document supports the following top-level keys:
 - `imports` *(list[object], optional)*: A list of type name aliases to simplify
   object and protobuf references within the expressions.
 - `rule` *(object, required)*: The entry point for the policy execution.
+- `verification` *(object, optional)*: Formal safety properties (`invariants`)
+  verified against the policy.
 
 ---
 
@@ -171,6 +173,40 @@ For more details on CEL optionals, refer to the [CEL optional proposal](https://
 
 ---
 
+### Formal Verification (`verification`)
+
+The `verification` block allows policy authors to declare custom safety
+properties that can be statically and mathematically verified using the CEL
+Verifier engine.
+
+Currently, it supports defining custom **invariants**:
+
+- `invariants` *(list[object], optional)*: A list of invariant declarations.
+
+Each invariant item contains:
+
+- `id` *(string, required)*: A unique identifier for the invariant.
+- `description` *(string, optional)*: Human-readable rationale for the
+  invariant.
+- `assume` *(string, optional)*: A CEL expression evaluating to `bool` that
+  defines the precondition constraining the input state space. Defaults to
+  `true` if omitted.
+- `assert` *(string, required)*: A CEL expression evaluating to `bool`
+  asserting the safety condition. It can reference the reserved identifier
+  `invariants.result`, which represents the evaluated return value of the
+  policy's `rule` graph.
+
+```yaml
+verification:
+  invariants:
+    - id: secure_port_required
+      description: "If external access is permitted, port must be 443"
+      assume: "request.external == true"
+      assert: "invariants.result == 'ALLOW' ? port == 443 : true"
+```
+
+---
+
 ### Type Imports (`imports`)
 
 The top-level `imports` list defines type alias references. These aliases