diff --git a/policy/src/main/java/dev/cel/policy/CelPolicy.java b/policy/src/main/java/dev/cel/policy/CelPolicy.java
index 19f6631d0..6756481df 100644
--- a/policy/src/main/java/dev/cel/policy/CelPolicy.java
+++ b/policy/src/main/java/dev/cel/policy/CelPolicy.java
@@ -15,6 +15,7 @@
 package dev.cel.policy;
 
 import static com.google.common.base.Preconditions.checkNotNull;
+import static java.util.stream.Collectors.joining;
 
 import com.google.auto.value.AutoOneOf;
 import com.google.auto.value.AutoValue;
@@ -53,6 +54,10 @@ public abstract class CelPolicy {
 
   public abstract ImmutableList<Import> imports();
 
+  public abstract ImmutableList<Invariant> invariants();
+
+  public abstract ImmutableList<Variable> verificationVariables();
+
   /** Creates a new builder to construct a {@link CelPolicy} instance. */
   public static Builder newBuilder() {
     return new AutoValue_CelPolicy.Builder()
@@ -74,6 +79,8 @@ public abstract static class Builder {
 
     public abstract Builder setDisplayName(ValueString displayName);
 
+    public abstract Rule rule();
+
     public abstract Builder setRule(Rule rule);
 
     public abstract Builder setPolicySource(CelPolicySource policySource);
@@ -90,6 +97,14 @@ public List<Import> imports() {
       return Collections.unmodifiableList(importList);
     }
 
+    abstract ImmutableList<Invariant> invariants();
+
+    abstract ImmutableList.Builder<Invariant> invariantsBuilder();
+
+    abstract ImmutableList<Variable> verificationVariables();
+
+    abstract ImmutableList.Builder<Variable> verificationVariablesBuilder();
+
     public Map<String, Object> metadata() {
       return Collections.unmodifiableMap(metadata);
     }
@@ -106,6 +121,24 @@ public Builder addImports(Collection<Import> values) {
       return this;
     }
 
+    @CanIgnoreReturnValue
+    public Builder addInvariant(Invariant value) {
+      invariantsBuilder().add(value);
+      return this;
+    }
+
+    @CanIgnoreReturnValue
+    public Builder addVerificationVariable(Variable value) {
+      verificationVariablesBuilder().add(value);
+      return this;
+    }
+
+    @CanIgnoreReturnValue
+    public Builder addVerificationVariables(Collection<Variable> values) {
+      verificationVariablesBuilder().addAll(values);
+      return this;
+    }
+
     @CanIgnoreReturnValue
     public Builder putMetadata(String key, Object value) {
       metadata.put(key, value);
@@ -328,4 +361,115 @@ public static Import create(long id, ValueString name) {
       return new AutoValue_CelPolicy_Import(id, name);
     }
   }
+
+  /**
+   * Invariant declares a required logical property that must hold true under specified
+   * preconditions.
+   */
+  @AutoValue
+  public abstract static class Invariant {
+    public abstract long id();
+
+    public abstract ValueString invariantId();
+
+    public abstract Optional<ValueString> description();
+
+    public abstract ImmutableList<ValueString> assume();
+
+    public abstract ImmutableList<ValueString> assertClause();
+
+    public String assumeSourceString() {
+      if (assume().isEmpty()) {
+        return "true";
+      }
+      if (assume().size() == 1) {
+        return assume().get(0).value();
+      }
+      return assume().stream().map(v -> "(" + v.value() + ")").collect(joining(" && "));
+    }
+
+    public String assertSourceString() {
+      if (assertClause().isEmpty()) {
+        return "true";
+      }
+      if (assertClause().size() == 1) {
+        return assertClause().get(0).value();
+      }
+      return assertClause().stream().map(v -> "(" + v.value() + ")").collect(joining(" && "));
+    }
+
+    /** Builder for {@link Invariant}. */
+    @AutoValue.Builder
+    public abstract static class Builder implements RequiredFieldsChecker {
+      public abstract Builder setId(long value);
+
+      abstract Optional<ValueString> invariantId();
+
+      abstract ImmutableList<ValueString> assume();
+
+      abstract ImmutableList.Builder<ValueString> assumeBuilder();
+
+      abstract ImmutableList<ValueString> assertClause();
+
+      abstract ImmutableList.Builder<ValueString> assertClauseBuilder();
+
+      public abstract Builder setInvariantId(ValueString value);
+
+      public abstract Builder setDescription(ValueString value);
+
+      public Builder setAssume(ValueString value) {
+        return setAssume(ImmutableList.of(value));
+      }
+
+      abstract Builder setAssume(ImmutableList<ValueString> values);
+
+      @CanIgnoreReturnValue
+      public Builder addAssume(ValueString value) {
+        assumeBuilder().add(value);
+        return this;
+      }
+
+      @CanIgnoreReturnValue
+      public Builder addAssume(Iterable<ValueString> values) {
+        assumeBuilder().addAll(values);
+        return this;
+      }
+
+      public Builder setAssertClause(ValueString value) {
+        return setAssertClause(ImmutableList.of(value));
+      }
+
+      abstract Builder setAssertClause(ImmutableList<ValueString> values);
+
+      @CanIgnoreReturnValue
+      public Builder addAssertClause(ValueString value) {
+        assertClauseBuilder().add(value);
+        return this;
+      }
+
+      @CanIgnoreReturnValue
+      public Builder addAssertClause(Iterable<ValueString> values) {
+        assertClauseBuilder().addAll(values);
+        return this;
+      }
+
+      @Override
+      public ImmutableList<RequiredField> requiredFields() {
+        return ImmutableList.of(
+            RequiredField.of("id", this::invariantId),
+            RequiredField.of(
+                "assert",
+                () ->
+                    assertClause().isEmpty()
+                        ? Optional.empty()
+                        : Optional.of(assertClause().get(0))));
+      }
+
+      public abstract Invariant build();
+    }
+
+    public static Builder newBuilder(long id) {
+      return new AutoValue_CelPolicy_Invariant.Builder().setId(id);
+    }
+  }
 }
diff --git a/policy/src/main/java/dev/cel/policy/CelPolicyYamlParser.java b/policy/src/main/java/dev/cel/policy/CelPolicyYamlParser.java
index 18b406af0..408c86247 100644
--- a/policy/src/main/java/dev/cel/policy/CelPolicyYamlParser.java
+++ b/policy/src/main/java/dev/cel/policy/CelPolicyYamlParser.java
@@ -15,6 +15,7 @@
 package dev.cel.policy;
 
 import static com.google.common.base.Preconditions.checkNotNull;
+import static com.google.common.collect.ImmutableSet.toImmutableSet;
 import static dev.cel.common.formats.YamlHelper.ERROR;
 import static dev.cel.common.formats.YamlHelper.assertRequiredFields;
 import static dev.cel.common.formats.YamlHelper.assertYamlType;
@@ -28,6 +29,7 @@
 import dev.cel.common.formats.YamlParserContextImpl;
 import dev.cel.common.internal.CelCodePointArray;
 import dev.cel.policy.CelPolicy.Import;
+import dev.cel.policy.CelPolicy.Invariant;
 import dev.cel.policy.CelPolicy.Match;
 import dev.cel.policy.CelPolicy.Match.Result;
 import dev.cel.policy.CelPolicy.Variable;
@@ -47,6 +49,8 @@ final class CelPolicyYamlParser implements CelPolicyParser {
       Match.newBuilder(0).setCondition(ERROR_VALUE).setResult(Result.ofOutput(ERROR_VALUE)).build();
   private static final Variable ERROR_VARIABLE =
       Variable.newBuilder().setExpression(ERROR_VALUE).setName(ERROR_VALUE).build();
+  private static final Invariant ERROR_INVARIANT =
+      Invariant.newBuilder(0).setInvariantId(ERROR_VALUE).setAssertClause(ERROR_VALUE).build();
 
   private final TagVisitor<Node> tagVisitor;
   private final boolean enableSimpleVariables;
@@ -137,17 +141,82 @@ public CelPolicy parsePolicy(PolicyParserContext<Node> ctx, Node node) {
           case "rule":
             policyBuilder.setRule(parseRule(ctx, policyBuilder, valueNode));
             break;
+          case "verification":
+            parseVerification(policyBuilder, ctx, valueNode);
+            break;
           default:
             tagVisitor.visitPolicyTag(ctx, keyId, fieldName, valueNode, policyBuilder);
             break;
         }
       }
 
+      ImmutableSet<String> ruleVarNames =
+          policyBuilder.rule().variables().stream()
+              .map(CelPolicy.Variable::name)
+              .filter(name -> !name.equals(ERROR_VALUE))
+              .map(ValueString::value)
+              .collect(toImmutableSet());
+      for (Variable verVar : policyBuilder.verificationVariables()) {
+        if (!verVar.name().equals(ERROR_VALUE)
+            && ruleVarNames.contains(verVar.name().value())) {
+          ctx.reportError(
+              verVar.name().id(),
+              "Duplicate variable name '"
+                  + verVar.name().value()
+                  + "' in verification.variables; already defined in rule.variables");
+        }
+      }
+
       return policyBuilder
           .setPolicySource(policySource.toBuilder().setPositionsMap(ctx.getIdToOffsetMap()).build())
           .build();
     }
 
+    private void parseVerification(
+        CelPolicy.Builder policyBuilder, PolicyParserContext<Node> ctx, Node node) {
+      long id = ctx.collectMetadata(node);
+      if (!assertYamlType(ctx, id, node, YamlNodeType.MAP)) {
+        return;
+      }
+      MappingNode mappingNode = (MappingNode) node;
+      for (NodeTuple nodeTuple : mappingNode.getValue()) {
+        Node key = nodeTuple.getKeyNode();
+        long keyId = ctx.collectMetadata(key);
+        if (!assertYamlType(ctx, keyId, key, YamlNodeType.STRING, YamlNodeType.TEXT)) {
+          continue;
+        }
+        String fieldName = ((ScalarNode) key).getValue();
+        Node valueNode = nodeTuple.getValueNode();
+        switch (fieldName) {
+          case "invariants": {
+            long valueId = ctx.collectMetadata(valueNode);
+            if (!assertYamlType(ctx, valueId, valueNode, YamlNodeType.LIST)) {
+              continue;
+            }
+            SequenceNode invariantListNode = (SequenceNode) valueNode;
+            for (Node invariantNode : invariantListNode.getValue()) {
+              policyBuilder.addInvariant(parseInvariant(ctx, policyBuilder, invariantNode));
+            }
+            break;
+          }
+          case "variables": {
+            long valueId = ctx.collectMetadata(valueNode);
+            if (!assertYamlType(ctx, valueId, valueNode, YamlNodeType.LIST)) {
+              continue;
+            }
+            SequenceNode variableListNode = (SequenceNode) valueNode;
+            for (Node varNode : variableListNode.getValue()) {
+              policyBuilder.addVerificationVariable(parseVariable(ctx, policyBuilder, varNode));
+            }
+            break;
+          }
+          default:
+            ctx.reportError(keyId, "Unexpected key in verification block: " + fieldName);
+            break;
+        }
+      }
+    }
+
     private void parseImports(
         CelPolicy.Builder policyBuilder, PolicyParserContext<Node> ctx, Node node) {
       long id = ctx.collectMetadata(node);
@@ -409,6 +478,82 @@ private Variable parseVariableObject(
       return builder.build();
     }
 
+    @Override
+    public CelPolicy.Invariant parseInvariant(
+        PolicyParserContext<Node> ctx, CelPolicy.Builder policyBuilder, Node node) {
+      long id = ctx.collectMetadata(node);
+      Invariant.Builder builder = Invariant.newBuilder(id);
+      if (!assertYamlType(ctx, id, node, YamlNodeType.MAP)) {
+        return ERROR_INVARIANT;
+      }
+
+      MappingNode invariantMap = (MappingNode) node;
+      for (NodeTuple nodeTuple : invariantMap.getValue()) {
+        Node keyNode = nodeTuple.getKeyNode();
+        long keyId = ctx.collectMetadata(keyNode);
+        if (!assertYamlType(ctx, keyId, keyNode, YamlNodeType.STRING, YamlNodeType.TEXT)) {
+          continue;
+        }
+        Node valueNode = nodeTuple.getValueNode();
+        String keyName = ((ScalarNode) keyNode).getValue();
+        switch (keyName) {
+          case "id":
+            builder.setInvariantId(ctx.newYamlString(valueNode));
+            break;
+          case "description":
+            builder.setDescription(ctx.newYamlString(valueNode));
+            break;
+          case "assume": {
+            if (!assertYamlType(
+                ctx,
+                ctx.collectMetadata(valueNode),
+                valueNode,
+                YamlNodeType.STRING,
+                YamlNodeType.TEXT,
+                YamlNodeType.LIST)) {
+              break;
+            }
+            if (valueNode instanceof SequenceNode) {
+              for (Node itemNode : ((SequenceNode) valueNode).getValue()) {
+                builder.addAssume(ctx.newSourceString(itemNode));
+              }
+            } else {
+              builder.addAssume(ctx.newSourceString(valueNode));
+            }
+            break;
+          }
+          case "assert": {
+            if (!assertYamlType(
+                ctx,
+                ctx.collectMetadata(valueNode),
+                valueNode,
+                YamlNodeType.STRING,
+                YamlNodeType.TEXT,
+                YamlNodeType.LIST)) {
+              break;
+            }
+            if (valueNode instanceof SequenceNode) {
+              for (Node itemNode : ((SequenceNode) valueNode).getValue()) {
+                builder.addAssertClause(ctx.newSourceString(itemNode));
+              }
+            } else {
+              builder.addAssertClause(ctx.newSourceString(valueNode));
+            }
+            break;
+          }
+          default:
+            ctx.reportError(keyId, "Unexpected key in invariant block: " + keyName);
+            break;
+        }
+      }
+
+      if (!assertRequiredFields(ctx, id, builder.getMissingRequiredFieldNames())) {
+        return ERROR_INVARIANT;
+      }
+
+      return builder.build();
+    }
+
     private ParserImpl(
         TagVisitor<Node> tagVisitor,
         boolean enableSimpleVariables,
diff --git a/policy/src/main/java/dev/cel/policy/PolicyParserContext.java b/policy/src/main/java/dev/cel/policy/PolicyParserContext.java
index 204bf591f..d06167139 100644
--- a/policy/src/main/java/dev/cel/policy/PolicyParserContext.java
+++ b/policy/src/main/java/dev/cel/policy/PolicyParserContext.java
@@ -16,6 +16,7 @@
 
 import com.google.auto.value.AutoValue;
 import dev.cel.common.formats.ParserContext;
+import dev.cel.policy.CelPolicy.Invariant;
 import dev.cel.policy.CelPolicy.Match;
 import dev.cel.policy.CelPolicy.Rule;
 import dev.cel.policy.CelPolicy.Variable;
@@ -51,4 +52,6 @@ static NewPolicyMetadata create(CelPolicySource source, long id) {
   Match parseMatch(PolicyParserContext<T> ctx, CelPolicy.Builder policyBuilder, T node);
 
   Variable parseVariable(PolicyParserContext<T> ctx, CelPolicy.Builder policyBuilder, T node);
+
+  Invariant parseInvariant(PolicyParserContext<T> ctx, CelPolicy.Builder policyBuilder, T node);
 }
diff --git a/policy/src/test/java/dev/cel/policy/BUILD.bazel b/policy/src/test/java/dev/cel/policy/BUILD.bazel
index 5157e0c74..6a76cf3b0 100644
--- a/policy/src/test/java/dev/cel/policy/BUILD.bazel
+++ b/policy/src/test/java/dev/cel/policy/BUILD.bazel
@@ -8,9 +8,7 @@ package(
 java_library(
     name = "tests",
     testonly = True,
-    srcs = glob(
-        ["*.java"],
-    ),
+    srcs = glob(["*.java"]),
     data = [
         "@cel_policy//conformance:testdata",
     ],
diff --git a/policy/src/test/java/dev/cel/policy/CelPolicyYamlParserTest.java b/policy/src/test/java/dev/cel/policy/CelPolicyYamlParserTest.java
index 2a2c47a98..aaa30518a 100644
--- a/policy/src/test/java/dev/cel/policy/CelPolicyYamlParserTest.java
+++ b/policy/src/test/java/dev/cel/policy/CelPolicyYamlParserTest.java
@@ -22,6 +22,8 @@
 import com.google.testing.junit.testparameterinjector.TestParameterInjector;
 import dev.cel.common.formats.ValueString;
 import dev.cel.policy.CelPolicy.Import;
+import dev.cel.policy.CelPolicy.Invariant;
+import dev.cel.policy.CelPolicy.Variable;
 import dev.cel.policy.PolicyTestHelper.TestYamlPolicy;
 import dev.cel.policy.testing.K8sTagHandler;
 import org.junit.Test;
@@ -194,6 +196,115 @@ public void parseYamlPolicy_errors(@TestParameter PolicyParseErrorTestCase testC
     assertThat(e).hasMessageThat().isEqualTo(testCase.expectedErrorMessage);
   }
 
+  @Test
+  public void policyBuilder_addInvariant() {
+    Invariant invariant =
+        Invariant.newBuilder(1L)
+            .setInvariantId(ValueString.newBuilder().setValue("id").build())
+            .setAssertClause(ValueString.newBuilder().setValue("true").build())
+            .build();
+    CelPolicy policy =
+        CelPolicy.newBuilder()
+            .setName(ValueString.of(0, "test"))
+            .setPolicySource(CelPolicySource.newBuilder("").build())
+            .addInvariant(invariant)
+            .build();
+    assertThat(policy.invariants()).containsExactly(invariant);
+  }
+
+  @Test
+  public void parseYamlPolicy_invariants_success() throws Exception {
+    String policySource =
+        "name: 'policy_with_invariants'\n"
+            + "verification:\n"
+            + "  invariants:\n"
+            + "    - id: 'inv_1'\n"
+            + "      description: 'invariant description'\n"
+            + "      assume: 'true'\n"
+            + "      assert: 'rule.result == true'";
+
+    CelPolicy policy = POLICY_PARSER.parse(policySource);
+
+    assertThat(policy.invariants()).hasSize(1);
+    Invariant invariant = Iterables.getOnlyElement(policy.invariants());
+    assertThat(invariant.invariantId().value()).isEqualTo("inv_1");
+    assertThat(invariant.description().get().value()).isEqualTo("invariant description");
+    assertThat(invariant.assume().get(0).value()).isEqualTo("true");
+    assertThat(invariant.assertClause().get(0).value()).isEqualTo("rule.result == true");
+  }
+
+  @Test
+  public void parseYamlPolicy_invariants_multiClauseLists_success() throws Exception {
+    String policySource =
+        "name: 'policy_with_list_invariants'\n"
+            + "verification:\n"
+            + "  invariants:\n"
+            + "    - id: 'inv_multi'\n"
+            + "      assume:\n"
+            + "        - 'x > 0'\n"
+            + "        - 'y > 0'\n"
+            + "      assert:\n"
+            + "        - 'rule.result == true'\n"
+            + "        - 'x + y > 0'";
+
+    CelPolicy policy = POLICY_PARSER.parse(policySource);
+
+    Invariant invariant = Iterables.getOnlyElement(policy.invariants());
+    assertThat(invariant.assumeSourceString()).isEqualTo("(x > 0) && (y > 0)");
+    assertThat(invariant.assertSourceString()).isEqualTo("(rule.result == true) && (x + y > 0)");
+  }
+
+  @Test
+  public void parseYamlPolicy_verificationVariables_success() throws Exception {
+    String policySource =
+        "name: 'policy_with_verification_vars'\n"
+            + "rule:\n"
+            + "  variables:\n"
+            + "    - name: rule_var\n"
+            + "      expression: 'true'\n"
+            + "verification:\n"
+            + "  variables:\n"
+            + "    - name: ver_var\n"
+            + "      expression: 'rule_var && true'\n"
+            + "  invariants:\n"
+            + "    - id: 'inv_var'\n"
+            + "      assume: 'variables.ver_var'\n"
+            + "      assert: 'rule.result == true'";
+
+    CelPolicy policy = POLICY_PARSER.parse(policySource);
+
+    assertThat(policy.verificationVariables()).hasSize(1);
+    Variable var = Iterables.getOnlyElement(policy.verificationVariables());
+    assertThat(var.name().value()).isEqualTo("ver_var");
+    assertThat(var.expression().value()).isEqualTo("rule_var && true");
+  }
+
+  @Test
+  public void parseYamlPolicy_verificationVariables_duplicateWithRuleVariables_throwsError() {
+    String policySource =
+        "name: 'policy_with_dup_vars'\n"
+            + "rule:\n"
+            + "  variables:\n"
+            + "    - name: dup_var\n"
+            + "      expression: 'true'\n"
+            + "verification:\n"
+            + "  variables:\n"
+            + "    - name: dup_var\n"
+            + "      expression: 'false'\n"
+            + "  invariants:\n"
+            + "    - id: 'inv_dup'\n"
+            + "      assume: 'variables.dup_var'\n"
+            + "      assert: 'rule.result == true'";
+
+    CelPolicyValidationException e =
+        assertThrows(CelPolicyValidationException.class, () -> POLICY_PARSER.parse(policySource));
+    assertThat(e)
+        .hasMessageThat()
+        .contains(
+            "Duplicate variable name 'dup_var' in verification.variables; already defined in"
+                + " rule.variables");
+  }
+
   private enum PolicyParseErrorTestCase {
     MALFORMED_YAML_DOCUMENT(
         "a:\na",
@@ -400,7 +511,70 @@ private enum PolicyParseErrorTestCase {
             + "- foo: bar",
         "ERROR: <input>:2:3: Invalid import key: foo, expected 'name'\n"
             + " | - foo: bar\n"
-            + " | ..^");
+            + " | ..^"),
+    UNSUPPORTED_VERIFICATION_TAG(
+        "verification:\n" //
+            + "  bad_key: true",
+        "ERROR: <input>:2:3: Unexpected key in verification block: bad_key\n"
+            + " |   bad_key: true\n"
+            + " | ..^"),
+    UNSUPPORTED_INVARIANT_TAG(
+        "verification:\n" //
+            + "  invariants:\n" //
+            + "    - id: foo\n" //
+            + "      bad_inv_key: true\n" //
+            + "      assert: 'true'",
+        "ERROR: <input>:4:7: Unexpected key in invariant block: bad_inv_key\n"
+            + " |       bad_inv_key: true\n"
+            + " | ......^"),
+    MISSING_INVARIANT_ID(
+        "verification:\n" //
+            + "  invariants:\n" //
+            + "    - assert: 'true'",
+        "ERROR: <input>:3:7: Missing required attribute(s): id\n"
+            + " |     - assert: 'true'\n"
+            + " | ......^"),
+    MISSING_INVARIANT_ASSERT(
+        "verification:\n" //
+            + "  invariants:\n" //
+            + "    - id: foo",
+        "ERROR: <input>:3:7: Missing required attribute(s): assert\n"
+            + " |     - id: foo\n"
+            + " | ......^"),
+    ILLEGAL_YAML_TYPE_ON_VERIFICATION_VALUE(
+        "verification: illegal\n",
+        "ERROR: <input>:1:15: Got yaml node type tag:yaml.org,2002:str, wanted type(s)"
+            + " [tag:yaml.org,2002:map]\n"
+            + " | verification: illegal\n"
+            + " | ..............^"),
+    ILLEGAL_YAML_TYPE_ON_VERIFICATION_MAP_KEY(
+        "verification:\n" + "  1: foo",
+        "ERROR: <input>:2:3: Got yaml node type tag:yaml.org,2002:int, wanted type(s)"
+            + " [tag:yaml.org,2002:str !txt]\n"
+            + " |   1: foo\n"
+            + " | ..^"),
+    ILLEGAL_YAML_TYPE_ON_INVARIANTS_VALUE(
+        "verification:\n" + "  invariants: illegal\n",
+        "ERROR: <input>:2:15: Got yaml node type tag:yaml.org,2002:str, wanted type(s)"
+            + " [tag:yaml.org,2002:seq]\n"
+            + " |   invariants: illegal\n"
+            + " | ..............^"),
+    ILLEGAL_YAML_TYPE_ON_INVARIANTS_LIST(
+        "verification:\n" + "  invariants:\n" + "    - illegal",
+        "ERROR: <input>:3:7: Got yaml node type tag:yaml.org,2002:str, wanted type(s)"
+            + " [tag:yaml.org,2002:map]\n"
+            + " |     - illegal\n"
+            + " | ......^"),
+    ILLEGAL_YAML_TYPE_ON_INVARIANT_MAP_KEY(
+        "verification:\n"
+            + "  invariants:\n"
+            + "    - 1: foo\n"
+            + "      id: 'hi'\n"
+            + "      assert: 'true'",
+        "ERROR: <input>:3:7: Got yaml node type tag:yaml.org,2002:int, wanted type(s)"
+            + " [tag:yaml.org,2002:str !txt]\n"
+            + " |     - 1: foo\n"
+            + " | ......^");
 
     private final String yamlPolicy;
     private final String expectedErrorMessage;
diff --git a/testing/src/test/resources/policy/verification/flawed_policy.yaml b/testing/src/test/resources/policy/verification/flawed_policy.yaml
new file mode 100644
index 000000000..1e276c899
--- /dev/null
+++ b/testing/src/test/resources/policy/verification/flawed_policy.yaml
@@ -0,0 +1,26 @@
+# Copyright 2026 Google LLC
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#    https://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+name: flawed_policy
+description: Tests detecting an invariant violation when a policy allows insecure output (port == 80), checking accurate counterexample generation.
+rule:
+  match:
+    - condition: port == 80
+      output: 'true'
+    - output: 'false'
+verification:
+  invariants:
+    - id: always_secure
+      description: Asserts that insecure output is never allowed, producing a counterexample when port is 80.
+      assert: rule.result == false
diff --git a/testing/src/test/resources/policy/verification/multi_invariant_policy.yaml b/testing/src/test/resources/policy/verification/multi_invariant_policy.yaml
new file mode 100644
index 000000000..11d11ad0f
--- /dev/null
+++ b/testing/src/test/resources/policy/verification/multi_invariant_policy.yaml
@@ -0,0 +1,37 @@
+# Copyright 2026 Google LLC
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#    https://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+name: multi_invariant_policy
+description: >
+  Tests multi-invariant verification where one invariant passes
+  ('admin_granted') and another is intentionally violated
+  ('viewer_granted'), checking mixed counterexample reporting.
+rule:
+  match:
+    - condition: role == 'admin' || role == 'editor'
+      output: 'true'
+    - output: 'false'
+verification:
+  invariants:
+    - id: admin_granted
+      description: Verifies that admin roles always evaluate to true.
+      assume: role == 'admin'
+      assert: rule.result == true
+    - id: viewer_granted
+      description: >
+        Intentionally false assertion that viewer roles are granted
+        permission, verifying that the solver detects the violation and
+        reports 'role = "viewer"' as the counterexample.
+      assume: role == 'viewer'
+      assert: rule.result == true
diff --git a/testing/src/test/resources/policy/verification/restricted_destinations_policy.yaml b/testing/src/test/resources/policy/verification/restricted_destinations_policy.yaml
new file mode 100644
index 000000000..bfaa812f4
--- /dev/null
+++ b/testing/src/test/resources/policy/verification/restricted_destinations_policy.yaml
@@ -0,0 +1,63 @@
+# Copyright 2026 Google LLC
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#    https://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+name: "restricted_destinations"
+description: >
+  Tests a realistic conformance policy verbatim with restricted
+  destinations, verifying security boundary assertions.
+rule:
+  variables:
+    - matches_origin_ip: "locationCode(origin.ip) == spec.origin"
+    - has_nationality: "has(request.auth.claims.nationality)"
+    - matches_nationality: "variables.has_nationality && request.auth.claims.nationality == spec.origin"
+    - matches_dest_ip: "locationCode(destination.ip) in spec.restricted_destinations"
+    - matches_dest_label: "resource.labels.location in spec.restricted_destinations"
+    - matches_dest: "variables.matches_dest_ip || variables.matches_dest_label"
+  match:
+    - condition: "variables.matches_nationality && variables.matches_dest"
+      output: "true"
+    - condition: "!variables.has_nationality && variables.matches_origin_ip && variables.matches_dest"
+      output: "true"
+    - output: "false"
+verification:
+  variables:
+    - is_prohibited_origin_ip: "!variables.has_nationality && variables.matches_origin_ip"
+    - is_unrestricted_dest: "!variables.matches_dest_ip && !variables.matches_dest_label"
+  invariants:
+    - id: restricted_by_nationality_prohibited
+      description: >
+        Verifies that requests to restricted destinations from users with
+        matching origin nationality are prohibited.
+      assume:
+        - "variables.matches_nationality"
+        - "variables.matches_dest"
+      assert:
+        - "rule.result == true"
+    - id: restricted_by_origin_ip_prohibited
+      description: >
+        Verifies that requests to restricted destinations from users without
+        nationality claims but matching origin IP are prohibited.
+      assume:
+        - "variables.is_prohibited_origin_ip"
+        - "variables.matches_dest"
+      assert:
+        - "rule.result == true"
+    - id: unrestricted_destination_allowed
+      description: >
+        Verifies that requests to destinations not in the restricted list
+        and without restricted labels are allowed ('false').
+      assume:
+        - "variables.is_unrestricted_dest"
+      assert:
+        - "rule.result == false"
diff --git a/testing/src/test/resources/policy/verification/secure_resource_access.yaml b/testing/src/test/resources/policy/verification/secure_resource_access.yaml
new file mode 100644
index 000000000..375957491
--- /dev/null
+++ b/testing/src/test/resources/policy/verification/secure_resource_access.yaml
@@ -0,0 +1,38 @@
+# Copyright 2026 Google LLC
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#    https://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+name: secure_resource_access
+description: >
+  Tests verifying security invariants across policy variables and protobuf
+  message fields ('test_all_types.repeated_string').
+rule:
+  variables:
+    - is_admin: "'admin' in test_all_types.repeated_string"
+    - is_break_glass: "test_all_types.single_string != ''"
+  match:
+    - condition: variables.is_admin && variables.is_break_glass
+      output: 'true'
+    - output: 'false'
+verification:
+  variables:
+    - is_unprivileged: "!('admin' in test_all_types.repeated_string)"
+  invariants:
+    - id: no_unprivileged_break_glass
+      description: >
+        Verifies that unprivileged users without the admin role can never
+        trigger break-glass access.
+      assume:
+        - "variables.is_unprivileged"
+      assert:
+        - "rule.result == false"
diff --git a/testing/src/test/resources/policy/verification/workload_admission_fixed.yaml b/testing/src/test/resources/policy/verification/workload_admission_fixed.yaml
new file mode 100644
index 000000000..d6d3cf92a
--- /dev/null
+++ b/testing/src/test/resources/policy/verification/workload_admission_fixed.yaml
@@ -0,0 +1,57 @@
+# Copyright 2026 Google LLC
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#    https://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+name: "workload_admission_fixed"
+description: "Controls deployment of workloads to Kubernetes clusters."
+rule:
+  variables:
+    - is_cluster_admin: "is_admin"
+    - is_namespace_owner: "is_owner"
+    - is_privileged_container: "is_privileged"
+    - is_prod_cluster: "is_prod"
+    - has_security_approval: "has_approval"
+
+  match:
+    # Hard DENY unapproved privileged containers in prod.
+    - condition: "variables.is_privileged_container && variables.is_prod_cluster && !variables.has_security_approval"
+      output: "'DENY'"
+      explanation: "'Privileged containers in production require explicit security approval.'"
+
+    # Break-glass admin bypass (Now safely guarded)
+    - condition: "variables.is_cluster_admin"
+      output: "'ALLOW'"
+
+    # Namespace owners
+    - condition: "variables.is_namespace_owner"
+      output: "'ALLOW'"
+
+    # Standard non-privileged deployments
+    - condition: "!variables.is_privileged_container"
+      output: "'ALLOW'"
+
+    # Default Deny
+    - output: "'DENY'"
+
+verification:
+  invariants:
+    - id: universal_no_unapproved_privileged_prod
+      description: >
+        Guarantees that NO ONE can deploy a privileged container
+        to production without explicit security approval, including admins.
+      assume:
+        - "variables.is_privileged_container"
+        - "variables.is_prod_cluster"
+        - "!variables.has_security_approval"
+      assert:
+        - "rule.result == 'DENY'"
diff --git a/testing/src/test/resources/policy/verification/workload_admission_flawed.yaml b/testing/src/test/resources/policy/verification/workload_admission_flawed.yaml
new file mode 100644
index 000000000..3ca591a09
--- /dev/null
+++ b/testing/src/test/resources/policy/verification/workload_admission_flawed.yaml
@@ -0,0 +1,67 @@
+# Copyright 2026 Google LLC
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#    https://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+name: "workload_admission_flawed"
+description: >
+  Controls deployment of workloads to Kubernetes clusters.
+  Note: This is an intentional buggy example.
+  The fixed example is shown in workload_admission_fixed.
+rule:
+  variables:
+    - is_cluster_admin: "is_admin"
+    - is_namespace_owner: "is_owner"
+    - is_privileged_container: "is_privileged"
+    - is_prod_cluster: "is_prod"
+    - has_security_approval: "has_approval"
+
+  match:
+    # Break-glass admin bypass
+    # BUG: This completely bypasses the production restriction for privileged containers below!
+    - condition: "variables.is_cluster_admin"
+      output: "'ALLOW'"
+
+    # Namespace owners can deploy workloads to their namespace
+    # BUG: The author forgot to enforce the privileged container rule for namespace owners!
+    - condition: "variables.is_namespace_owner"
+      output: "'ALLOW'"
+
+    # Strictly restrict privileged containers in production
+    - condition: "variables.is_privileged_container && variables.is_prod_cluster"
+      rule:
+        match:
+          - condition: "variables.has_security_approval"
+            output: "'ALLOW'"
+          - output: "'DENY'"
+            explanation: >
+              'Privileged containers in production require explicit security approval.'
+
+    # Standard non-privileged deployments
+    - condition: "!variables.is_privileged_container"
+      output: "'ALLOW'"
+
+    # Default Deny
+    - output: "'DENY'"
+
+verification:
+  invariants:
+    - id: universal_no_unapproved_privileged_prod
+      description: >
+        Mathematically guarantees that NO ONE can deploy a privileged container
+        to production without explicit security approval, including admins.
+      assume:
+        - "variables.is_privileged_container"
+        - "variables.is_prod_cluster"
+        - "!variables.has_security_approval"
+      assert:
+        - "rule.result == 'DENY'"
diff --git a/verifier/BUILD.bazel b/verifier/BUILD.bazel
index 41837d1bc..1c2e5adfa 100644
--- a/verifier/BUILD.bazel
+++ b/verifier/BUILD.bazel
@@ -17,6 +17,7 @@ java_library(
 
 java_library(
     name = "policy_verifier_factory",
+    compatible_with = [],
     exports = ["//verifier/src/main/java/dev/cel/verifier:policy_verifier_factory"],
 )
 
diff --git a/verifier/README.md b/verifier/README.md
index c10ce06eb..bf98643af 100644
--- a/verifier/README.md
+++ b/verifier/README.md
@@ -34,18 +34,26 @@ properties about your expressions.
 
 *   **Satisfiability & Validity Proving:** Check if an expression can ever
     evaluate to `true` (satisfiability) or if it is guaranteed to always be
-    `true` (validity).
+    `true` (validity). When checking satisfiability (`isSatisfiable`), the
+    verifier produces a satisfying model (witness assignments) showing concrete
+    inputs that make the expression true.
 *   **Logical Equivalence:** Prove that two different ASTs or Policies are
     semantically identical.
 *   **Bounded Model Checking (BMC):** Safely verify list and map comprehensions
     (`all`, `exists`, `map`, `filter`) by statically unrolling them up to a
     configurable limit.
-*   **Counterexample Generation:** When verification fails (e.g., two
-    expressions are not equivalent), the verifier generates a human-readable
-    counterexample showing the inputs that caused the mismatch.
+*   **Counterexample & Witness Generation:** When validity (`isAlwaysTrue`) or
+    equivalence verification fails, the verifier generates a human-readable
+    counterexample showing the inputs that caused the violation. When checking
+    satisfiability (`isSatisfiable`), it generates concrete variable assignments
+    (satisfying model / witness) showing the inputs that satisfy the condition.
 *   **Partial Evaluation (Unknowns) Support:** Define variables that are
     permitted to evaluate to `Unknown` during verification, mirroring CEL's
     runtime partial evaluation.
+*   **Custom Invariants Verification:** Allows policy authors to define safety
+    invariants (e.g., "port must always be secure if external access is
+    allowed") and mathematically prove that the policy never violates them
+    across all possible input states.
 
 ```java
 CelVerifier verifier = CelVerifierFactory.newVerifier()
@@ -59,9 +67,6 @@ CelVerifier verifier = CelVerifierFactory.newVerifier()
 
 The following features are planned for future releases:
 
-*   **Custom Invariants Verification:** Allows policy authors to define safety
-    invariants (e.g., "port must always be secure if external access is
-    allowed") and mathematically prove that the policy never violates them.
 *   **Deep Reachability Analysis:** Statically analyzes nested policy rules
     to detect unreachable execution paths (dead code) that can never be
     executed under any input.
@@ -115,17 +120,21 @@ public class VerifierExample {
       return;
     }
 
-    if (result.status() == VerificationStatus.VERIFIED) {
-      System.out.println("Expressions are logically equivalent!");
-    } else if (result.status() == VerificationStatus.VIOLATED) {
-      System.out.println(result.message());
-      // Example output if expressions were NOT equivalent:
-      // Equivalence violation detected. Counterexample input:
-      //   x = ...
-    } else {
-      // INCONCLUSIVE means the solver could not positively confirm VERIFIED or VIOLATED
-      // due to things like loop truncation (BMC) or uninterpreted functions.
-      System.out.println("Verification was inconclusive: " + result.message());
+    switch (result.status()) {
+      case VERIFIED:
+        System.out.println("Expressions are logically equivalent!");
+        break;
+      case VIOLATED:
+        System.out.println(result.message());
+        // Example output if expressions were NOT equivalent:
+        // Equivalence violation detected. Counterexample input:
+        //   x = ...
+        break;
+      case INCONCLUSIVE:
+        // INCONCLUSIVE means the solver could not positively confirm VERIFIED or VIOLATED
+        // due to things like loop truncation (BMC) or uninterpreted functions.
+        System.out.println("Verification was inconclusive: " + result.message());
+        break;
     }
   }
 }
@@ -153,7 +162,7 @@ import dev.cel.verifier.CelVerifier;
 import dev.cel.verifier.CelVerifierFactory;
 
 public class PolicyVerifierExample {
-  private static final Cel CEL = CelFactory.standardCelBuilder()
+  private static final Cel CEL = CelFactory.plannerCelBuilder()
       .addVar("role", SimpleType.STRING)
       .addVar("country", SimpleType.STRING)
       .addVar("port", SimpleType.INT)
@@ -206,18 +215,150 @@ public class PolicyVerifierExample {
       return;
     }
 
-    if (result.status() == VerificationStatus.VERIFIED) {
-      System.out.println("Policies are equivalent!");
-    } else if (result.status() == VerificationStatus.VIOLATED) {
-      System.out.println("Refactoring bug detected!");
-      System.out.println(result.message());
-      // Output:
-      // Equivalence violation detected. Counterexample input:
-      //   country = "a"
-      //   role = "editor"
-      //   port = 443
-    } else {
-      System.out.println("Verification was inconclusive: " + result.message());
+    switch (result.status()) {
+      case VERIFIED:
+        System.out.println("Policies are equivalent!");
+        break;
+      case VIOLATED:
+        System.out.println("Refactoring bug detected!");
+        System.out.println(result.message());
+        // Output:
+        // Equivalence violation detected. Counterexample input:
+        //   country = "a"
+        //   role = "editor"
+        //   port = 443
+        break;
+      case INCONCLUSIVE:
+        System.out.println("Verification was inconclusive: " + result.message());
+        break;
+    }
+  }
+}
+```
+
+### 3. Satisfiability Checking & Witness Generation
+
+When checking whether an expression is satisfiable using `isSatisfiable`, the
+verifier returns `VERIFIED` if there exists at least one input combination
+where the expression evaluates to `true`. Furthermore, `result.message()`
+provides concrete satisfying model assignments (witness/test case generation).
+
+```java
+import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.types.SimpleType;
+import dev.cel.compiler.CelCompiler;
+import dev.cel.compiler.CelCompilerFactory;
+import dev.cel.verifier.CelVerificationResult;
+import dev.cel.verifier.CelVerificationResult.VerificationStatus;
+import dev.cel.verifier.CelVerifier;
+import dev.cel.verifier.CelVerifierFactory;
+
+public class SatisfiabilityExample {
+  public static void main(String[] args) throws Exception {
+    CelCompiler compiler = CelCompilerFactory.standardCelCompilerBuilder()
+        .addVar("role", SimpleType.STRING)
+        .addVar("port", SimpleType.INT)
+        .build();
+
+    // Check if an authorization condition can ever be met
+    CelAbstractSyntaxTree ast =
+        compiler.compile("role == 'editor' && port > 1024 && port < 65535").getAst();
+
+    CelVerifier verifier = CelVerifierFactory.newVerifier().build();
+    CelVerificationResult result = verifier.isSatisfiable(ast);
+
+    switch (result.status()) {
+      case VERIFIED:
+        System.out.println("Condition is satisfiable!");
+        System.out.println(result.message());
+        // Output:
+        // Condition is satisfiable. Satisfying input:
+        //   port = 1025
+        //   role = "editor"
+        break;
+      case VIOLATED:
+        System.out.println("Condition is completely unsatisfiable.");
+        break;
+      case INCONCLUSIVE:
+        System.out.println("Verification was inconclusive: " + result.message());
+        break;
+    }
+  }
+}
+```
+
+### 4. Policy Invariants Verification
+
+You can verify that custom invariants (`assume` preconditions and `assert`
+clauses) declared on a `CelPolicy` hold mathematically across all possible
+input states. The reserved `rule.result` identifier matches the return
+value of the policy.
+
+```java
+import com.google.common.collect.ImmutableMap;
+import dev.cel.bundle.Cel;
+import dev.cel.bundle.CelFactory;
+import dev.cel.common.types.SimpleType;
+import dev.cel.policy.CelPolicy;
+import dev.cel.policy.CelPolicyCompiler;
+import dev.cel.policy.CelPolicyCompilerFactory;
+import dev.cel.policy.CelPolicyParser;
+import dev.cel.policy.CelPolicyParserFactory;
+import dev.cel.verifier.CelPolicyVerifier;
+import dev.cel.verifier.CelPolicyVerifierFactory;
+import dev.cel.verifier.CelVerificationResult;
+import dev.cel.verifier.CelVerificationResult.VerificationStatus;
+import dev.cel.verifier.CelVerifier;
+import dev.cel.verifier.CelVerifierFactory;
+
+public class InvariantsExample {
+  private static final Cel CEL = CelFactory.plannerCelBuilder()
+      .addVar("port", SimpleType.INT)
+      .build();
+
+  private static final CelPolicyParser PARSER = CelPolicyParserFactory.newYamlParserBuilder().build();
+
+  private static final CelPolicyCompiler POLICY_COMPILER =
+      CelPolicyCompilerFactory.newPolicyCompiler(CEL).build();
+
+  private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier().build();
+
+  private static final CelPolicyVerifier POLICY_VERIFIER =
+      CelPolicyVerifierFactory.newVerifier(POLICY_COMPILER, AST_VERIFIER).build();
+
+  public static void main(String[] args) throws Exception {
+    String yamlPolicy = """
+        name: secure_access_policy
+        rule:
+          match:
+            - condition: port == 80
+              output: 'true'
+            - output: 'false'
+        verification:
+          invariants:
+            - id: always_secure
+              assert:
+                - rule.result == false
+        """;
+
+    CelPolicy policy = PARSER.parse(yamlPolicy);
+    ImmutableMap<String, CelVerificationResult> results = POLICY_VERIFIER.verifyInvariants(policy);
+
+    CelVerificationResult result = results.get("always_secure");
+    switch (result.status()) {
+      case VERIFIED:
+        System.out.println("Invariant proven!");
+        break;
+      case VIOLATED:
+        System.out.println("Invariant violated!");
+        System.out.println(result.message());
+        // Output:
+        // Implication violation detected. Counterexample input:
+        //   port = 80
+        break;
+      case INCONCLUSIVE:
+        System.out.println("Verification was inconclusive: " + result.message());
+        break;
     }
   }
 }
diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
index 6cdb793db..792ac5d2d 100644
--- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
+++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
@@ -50,12 +50,14 @@ java_library(
         ":verifier",
         "//policy",
         "//policy:validation_exception",
+        "@maven//:com_google_guava_guava",
     ],
 )
 
 java_library(
     name = "policy_verifier_factory",
     srcs = ["CelPolicyVerifierFactory.java"],
+    compatible_with = [],
     tags = [
     ],
     deps = [
@@ -69,15 +71,23 @@ java_library(
 java_library(
     name = "policy_verifier_impl",
     srcs = ["CelPolicyVerifierImpl.java"],
+    compatible_with = [],
     tags = [
     ],
     deps = [
         ":policy_verifier",
         ":verifier",
+        ":z3_impl",
+        "//bundle:cel",
         "//common:cel_ast",
+        "//common:cel_source",
+        "//common:compiler_common",
+        "//common/formats:value_string",
         "//policy",
+        "//policy:compiled_rule",
         "//policy:compiler",
         "//policy:validation_exception",
+        "@maven//:com_google_guava_guava",
     ],
 )
 
diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
index 54049a1b5..255658136 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
@@ -116,6 +116,14 @@ BoolExpr isTrue(Expr<?> celValue) {
     return ctx.mkAnd(typeSystem.isBool(celValue), (BoolExpr) typeSystem.unwrapBool(celValue));
   }
 
+  /**
+   * Binds an identifier name in the symbol table to an already-translated value. Used to bind
+   * reserved policy symbols such as 'rule.result' to the composed policy graph.
+   */
+  void bindSymbol(String varName, TranslatedValue value) {
+    symbolTable.put(varName, value);
+  }
+
   TranslatedValue translate(CelAbstractSyntaxTree ast) {
     TranslatedValue result;
     CelBlock celBlock = CelBlock.extract(ast).orElse(null);
@@ -261,7 +269,7 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as
                   /* isApproximate= */ ctx.mkFalse());
             });
 
-    return TranslatedValue.create(tv.z3Expr(), celExpr, typeSystem, ctx.mkFalse());
+    return TranslatedValue.create(tv.z3Expr(), celExpr, typeSystem, tv.isApproximate());
   }
 
   private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast) {
diff --git a/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifier.java b/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifier.java
index f9ad77c93..70e1494f1 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifier.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifier.java
@@ -14,6 +14,7 @@
 
 package dev.cel.verifier;
 
+import com.google.common.collect.ImmutableMap;
 import dev.cel.policy.CelPolicy;
 import dev.cel.policy.CelPolicyValidationException;
 
@@ -27,4 +28,15 @@ public interface CelPolicyVerifier {
    */
   CelVerificationResult verifyEquivalence(CelPolicy policyA, CelPolicy policyB)
       throws CelPolicyValidationException, CelVerificationException;
+
+  /**
+   * Verifies all custom invariants defined in the policy against all possible input states.
+   *
+   * @return A map of invariant IDs to their verification results.
+   * @throws CelPolicyValidationException if the policy or any invariant fails compilation.
+   * @throws CelVerificationException if the verification check encounters an internal solver error.
+   */
+  ImmutableMap<String, CelVerificationResult> verifyInvariants(CelPolicy policy)
+      throws CelPolicyValidationException, CelVerificationException;
 }
+
diff --git a/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java b/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java
index 8cc145117..885201190 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java
@@ -14,7 +14,17 @@
 
 package dev.cel.verifier;
 
+import com.google.common.collect.ImmutableMap;
+import dev.cel.bundle.Cel;
+import dev.cel.bundle.CelBuilder;
 import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.CelIssue;
+import dev.cel.common.CelSource;
+import dev.cel.common.CelValidationException;
+import dev.cel.common.CelVarDecl;
+import dev.cel.common.formats.ValueString;
+import dev.cel.policy.CelCompiledRule;
+import dev.cel.policy.CelCompiledRule.CelCompiledVariable;
 import dev.cel.policy.CelPolicy;
 import dev.cel.policy.CelPolicyCompiler;
 import dev.cel.policy.CelPolicyValidationException;
@@ -22,6 +32,8 @@
 /** Implementation of CelPolicyVerifier using a CelVerifier. */
 final class CelPolicyVerifierImpl implements CelPolicyVerifier {
 
+  private static final String INVARIANTS_RESULT_IDENTIFIER = "rule.result";
+
   private final CelPolicyCompiler compiler;
   private final CelVerifier astVerifier;
 
@@ -56,4 +68,89 @@ public CelVerificationResult verifyEquivalence(CelPolicy policyA, CelPolicy poli
     CelAbstractSyntaxTree astB = compiler.compile(policyB);
     return astVerifier.verifyEquivalence(astA, astB);
   }
+
+  @Override
+  public ImmutableMap<String, CelVerificationResult> verifyInvariants(CelPolicy policy)
+      throws CelPolicyValidationException, CelVerificationException {
+    if (policy.invariants().isEmpty()) {
+      return ImmutableMap.of();
+    }
+
+    CelCompiledRule compiledRule = compiler.compileRule(policy);
+    CelAbstractSyntaxTree composedPolicyAst = compiler.compose(policy, compiledRule);
+
+    CelBuilder celBuilder = compiledRule.cel().toCelBuilder();
+    ImmutableMap.Builder<String, CelAbstractSyntaxTree> boundSymbolsBuilder =
+        ImmutableMap.builder();
+    for (CelCompiledVariable var : compiledRule.variables()) {
+      celBuilder.addVarDeclarations(var.celVarDecl());
+      boundSymbolsBuilder.put(var.celVarDecl().name(), var.ast());
+    }
+    boundSymbolsBuilder.put(INVARIANTS_RESULT_IDENTIFIER, composedPolicyAst);
+    celBuilder.addVarDeclarations(
+        CelVarDecl.newVarDeclaration(
+            INVARIANTS_RESULT_IDENTIFIER, composedPolicyAst.getResultType()));
+
+    Cel localCel = celBuilder.build();
+    for (CelPolicy.Variable variable : policy.verificationVariables()) {
+      ValueString expression = variable.expression();
+      CelAbstractSyntaxTree varAst;
+      try {
+        varAst = localCel.compile(expression.value()).getAst();
+      } catch (CelValidationException e) {
+        throw new CelPolicyValidationException(
+            CelIssue.toDisplayString(
+                e.getErrors(),
+                CelSource.newBuilder(expression.value())
+                    .setDescription("verification.variables." + variable.name().value())
+                    .build()));
+      }
+      String variableName = variable.name().value();
+      CelVarDecl newVariable =
+          CelVarDecl.newVarDeclaration("variables." + variableName, varAst.getResultType());
+      celBuilder.addVarDeclarations(newVariable);
+      boundSymbolsBuilder.put("variables." + variableName, varAst);
+      localCel = localCel.toCelBuilder().addVarDeclarations(newVariable).build();
+    }
+    Cel enrichedCel = celBuilder.build();
+    ImmutableMap<String, CelAbstractSyntaxTree> boundSymbols = boundSymbolsBuilder.buildOrThrow();
+
+    ImmutableMap.Builder<String, CelVerificationResult> resultsBuilder = ImmutableMap.builder();
+    for (CelPolicy.Invariant invariant : policy.invariants()) {
+      CelAbstractSyntaxTree assumeAst;
+      try {
+        assumeAst = enrichedCel.compile(invariant.assumeSourceString()).getAst();
+      } catch (CelValidationException e) {
+        throw new CelPolicyValidationException(
+            CelIssue.toDisplayString(
+                e.getErrors(),
+                CelSource.newBuilder(invariant.assumeSourceString())
+                    .setDescription("invariant." + invariant.invariantId().value() + ".assume")
+                    .build()));
+      }
+
+      CelAbstractSyntaxTree assertAst;
+      try {
+        assertAst = enrichedCel.compile(invariant.assertSourceString()).getAst();
+      } catch (CelValidationException e) {
+        throw new CelPolicyValidationException(
+            CelIssue.toDisplayString(
+                e.getErrors(),
+                CelSource.newBuilder(invariant.assertSourceString())
+                    .setDescription("invariant." + invariant.invariantId().value() + ".assert")
+                    .build()));
+      }
+
+      if (!(astVerifier instanceof CelVerifierZ3Impl)) {
+        throw new UnsupportedOperationException(
+            "Invariants verification requires Z3 verifier implementation.");
+      }
+      CelVerificationResult result =
+          ((CelVerifierZ3Impl) astVerifier)
+              .verifyImplication(assumeAst, assertAst, boundSymbols);
+      resultsBuilder.put(invariant.invariantId().value(), result);
+    }
+
+    return resultsBuilder.buildOrThrow();
+  }
 }
diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifier.java b/verifier/src/main/java/dev/cel/verifier/CelVerifier.java
index 32bffa1d3..0e80424f2 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelVerifier.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelVerifier.java
@@ -46,3 +46,5 @@ public interface CelVerifier {
   CelVerificationResult verifyEquivalence(CelAbstractSyntaxTree astA, CelAbstractSyntaxTree astB)
       throws CelVerificationException;
 }
+
+
diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
index 9d8b87e07..ce2705b56 100644
--- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
+++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
@@ -33,7 +33,10 @@
 import dev.cel.verifier.axioms.CelZ3FunctionAxiom;
 import dev.cel.verifier.axioms.CelZ3StandardAxioms;
 import java.time.Duration;
+import java.util.ArrayList;
 import java.util.Arrays;
+import java.util.List;
+import java.util.Map;
 import java.util.Optional;
 import org.jspecify.annotations.Nullable;
 
@@ -221,6 +224,95 @@ public CelVerificationResult verifyEquivalence(
     }
   }
 
+  CelVerificationResult verifyImplication(
+      CelAbstractSyntaxTree assumeAst,
+      CelAbstractSyntaxTree assertAst,
+      Map<String, CelAbstractSyntaxTree> boundSymbols)
+      throws CelVerificationException {
+    Preconditions.checkArgument(assumeAst.isChecked(), "assumeAst must be type-checked.");
+    Preconditions.checkArgument(assertAst.isChecked(), "assertAst must be type-checked.");
+    for (Map.Entry<String, CelAbstractSyntaxTree> entry : boundSymbols.entrySet()) {
+      Preconditions.checkArgument(
+          entry.getValue().isChecked(),
+          "boundSymbol AST for '%s' must be type-checked.",
+          entry.getKey());
+    }
+
+    try (Context ctx = new Context(ImmutableMap.of("model", "true"))) {
+      CelAstToZ3Translator translator =
+          new CelAstToZ3Translator(
+              ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider);
+
+      List<BoolExpr> taints = new ArrayList<>();
+      for (Map.Entry<String, CelAbstractSyntaxTree> entry : boundSymbols.entrySet()) {
+        TranslatedValue tv = translator.translate(entry.getValue());
+        translator.bindSymbol(entry.getKey(), tv);
+      }
+
+      TranslatedValue assumeTv = translator.translate(assumeAst);
+      TranslatedValue assertTv = translator.translate(assertAst);
+      taints.add(assumeTv.isApproximate());
+      taints.add(assertTv.isApproximate());
+
+      BoolExpr assumeCondition = translator.isTrue(assumeTv.z3Expr());
+      BoolExpr assertCondition = translator.isTrue(assertTv.z3Expr());
+      BoolExpr violationCondition = ctx.mkAnd(assumeCondition, ctx.mkNot(assertCondition));
+
+      BoolExpr combinedTaint = CelZ3TypeSystem.mkOrFlattened(ctx, taints);
+      BoolExpr unknownCondition =
+          ctx.mkOr(
+              translator.getTypeSystem().isUnknown(assumeTv.z3Expr()),
+              translator.getTypeSystem().isUnknown(assertTv.z3Expr()));
+
+      Solver solver = newSolver(ctx);
+      for (BoolExpr constraint : translator.getTypeConstraints()) {
+        solver.add(constraint);
+      }
+
+      SolverRunResult result =
+          runThreePassVerification(
+              ctx,
+              solver,
+              violationCondition,
+              combinedTaint,
+              unknownCondition,
+              translator,
+              /* checkTruncation= */ true);
+
+      switch (result.outcome) {
+        case EXACT_MATCH:
+          return CelVerificationResult.failed(
+              "Implication violation detected."
+                  + getCounterexampleString(
+                      ctx,
+                      translator.getTypeSystem(),
+                      result.model,
+                      /* isApproximate= */ false,
+                      /* isCounterexample= */ true));
+        case APPROXIMATE_MATCH:
+          return CelVerificationResult.inconclusive(
+              "Inconclusive: a counterexample may exist, but it depends on approximations, missing"
+                  + " theories, or loop bounds."
+                  + getCounterexampleString(
+                      ctx,
+                      translator.getTypeSystem(),
+                      result.model,
+                      /* isApproximate= */ true,
+                      /* isCounterexample= */ true));
+        case TRUNCATED:
+          return CelVerificationResult.inconclusive(
+              "Inconclusive: implication holds within the current loop unroll limit, but"
+                  + " may be violated for larger collections.");
+        case NO_MATCH:
+          return CelVerificationResult.verified();
+        case SOLVER_UNKNOWN:
+          return CelVerificationResult.inconclusive(
+              "Inconclusive: the solver returned unknown status (" + result.reason + ").");
+      }
+      throw new AssertionError("Unknown verification outcome: " + result.outcome);
+    }
+  }
+
   private CelVerificationResult checkSatisfiability(
       CelAbstractSyntaxTree ast, boolean searchForCounterexample) throws CelVerificationException {
     try (Context ctx = new Context(ImmutableMap.of("model", "true"))) {
diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel
index 03676eca6..9e7f0ed15 100644
--- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel
+++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel
@@ -12,6 +12,9 @@ java_library(
         ["**/*.java"],
     ),
     compatible_with = [],
+    data = [
+        "//testing:policy_test_resources",
+    ],
     deps = [
         "//bundle:cel",
         "//common:cel_ast",
@@ -37,6 +40,8 @@ java_library(
         "//policy:compiler_factory",
         "//policy:parser",
         "//policy:parser_factory",
+        "//policy:validation_exception",
+        "@bazel_tools//tools/java/runfiles",
         "@maven//:junit_junit",
         "@maven//:com_google_testparameterinjector_test_parameter_injector",
         "//:java_truth",
diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
index 2bc500bde..09f205f04 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
@@ -15,13 +15,18 @@
 package dev.cel.verifier;
 
 import static com.google.common.truth.Truth.assertThat;
+import static com.google.common.truth.Truth.assertWithMessage;
+import static org.junit.Assert.assertThrows;
 
+import com.google.common.collect.ImmutableMap;
 import com.google.testing.junit.testparameterinjector.TestParameter;
 import com.google.testing.junit.testparameterinjector.TestParameterInjector;
 import dev.cel.bundle.Cel;
 import dev.cel.bundle.CelFactory;
 import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.common.CelFunctionDecl;
 import dev.cel.common.CelOptions;
+import dev.cel.common.CelOverloadDecl;
 import dev.cel.common.types.SimpleType;
 import dev.cel.common.types.StructTypeReference;
 import dev.cel.expr.conformance.proto3.TestAllTypes;
@@ -37,6 +42,7 @@
 import dev.cel.policy.CelPolicyCompilerFactory;
 import dev.cel.policy.CelPolicyParser;
 import dev.cel.policy.CelPolicyParserFactory;
+import dev.cel.policy.CelPolicyValidationException;
 import dev.cel.verifier.CelVerificationResult.VerificationStatus;
 import org.junit.Before;
 import org.junit.Test;
@@ -49,8 +55,12 @@ public final class CelPolicyVerifierImplTest {
       CelPolicyParserFactory.newYamlParserBuilder().enableSimpleVariables(true).build();
 
   private static final Cel CEL =
-      CelFactory.standardCelBuilder()
-          .setOptions(CelOptions.current().populateMacroCalls(true).build())
+      CelFactory.plannerCelBuilder()
+          .setOptions(
+              CelOptions.current()
+                  .populateMacroCalls(true)
+                  .enableHeterogeneousNumericComparisons(true)
+                  .build())
           .setStandardMacros(CelStandardMacro.STANDARD_MACROS)
           .addCompilerLibraries(CelExtensions.bindings())
           .addMessageTypes(TestAllTypes.getDescriptor())
@@ -308,4 +318,382 @@ public void verifyEquivalence_celBlockSupport_cseOptimizer(
     assertThat(unparsed).startsWith("cel.@block");
     assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
   }
+
+  @Test
+  public void verifyInvariants_emptyInvariants_returnsEmptyMap() throws Exception {
+    String policySource =
+        "name: empty_policy\n" //
+            + "rule:\n" //
+            + "  match:\n" //
+            + "    - output: 'true'";
+    CelPolicy policy = PARSER.parse(policySource);
+
+    ImmutableMap<String, CelVerificationResult> results = VERIFIER.verifyInvariants(policy);
+
+    assertThat(results).isEmpty();
+  }
+
+  @Test
+  public void verifyInvariants_flawedPolicy_violationDetected() throws Exception {
+    CelPolicy policy =
+        PARSER.parse(VerifierTestHelper.loadVerificationPolicyYaml("flawed_policy.yaml"));
+
+    ImmutableMap<String, CelVerificationResult> results = VERIFIER.verifyInvariants(policy);
+
+    assertThat(results).containsKey("always_secure");
+    CelVerificationResult result = results.get("always_secure");
+    assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED);
+    assertThat(result.message()).containsMatch("port = 80");
+  }
+
+  @Test
+  public void verifyInvariants_secureResourceAccess_verified() throws Exception {
+    Cel extendedCel =
+        CEL.toCelBuilder()
+            .addVar("resource", SimpleType.DYN)
+            .build();
+    CelPolicyVerifier verifier =
+        CelPolicyVerifierFactory.newVerifier(
+                CelPolicyCompilerFactory.newPolicyCompiler(extendedCel).build(), AST_VERIFIER)
+            .build();
+
+    CelPolicy policy =
+        PARSER.parse(VerifierTestHelper.loadVerificationPolicyYaml("secure_resource_access.yaml"));
+
+    ImmutableMap<String, CelVerificationResult> results = verifier.verifyInvariants(policy);
+
+    assertThat(results).containsKey("no_unprivileged_break_glass");
+    assertThat(results.get("no_unprivileged_break_glass").status())
+        .isEqualTo(VerificationStatus.VERIFIED);
+  }
+
+  @Test
+  public void verifyInvariants_multipleInvariants_mixedResults() throws Exception {
+    CelPolicy policy =
+        PARSER.parse(VerifierTestHelper.loadVerificationPolicyYaml("multi_invariant_policy.yaml"));
+
+    ImmutableMap<String, CelVerificationResult> results = VERIFIER.verifyInvariants(policy);
+
+    assertThat(results).hasSize(2);
+    assertThat(results.get("admin_granted").status()).isEqualTo(VerificationStatus.VERIFIED);
+    assertThat(results.get("viewer_granted").status()).isEqualTo(VerificationStatus.VIOLATED);
+    assertThat(results.get("viewer_granted").message()).containsMatch("role = \"viewer\"");
+  }
+
+  @Test
+  public void verifyInvariants_invalidAssumeClause_throwsValidationException() throws Exception {
+    String policySource =
+        "name: invalid_assume\n" //
+            + "rule:\n" //
+            + "  match:\n" //
+            + "    - output: 'true'\n" //
+            + "verification:\n" //
+            + "  invariants:\n" //
+            + "    - id: bad_assume\n" //
+            + "      assume: non_existent_var == 123\n" //
+            + "      assert: rule.result == true";
+    CelPolicy policy = PARSER.parse(policySource);
+
+    assertThrows(CelPolicyValidationException.class, () -> VERIFIER.verifyInvariants(policy));
+  }
+
+  @Test
+  public void verifyInvariants_invalidAssertClause_throwsValidationException() throws Exception {
+    String policySource =
+        "name: invalid_assert\n" //
+            + "rule:\n" //
+            + "  match:\n" //
+            + "    - output: 'true'\n" //
+            + "verification:\n" //
+            + "  invariants:\n" //
+            + "    - id: bad_assert\n" //
+            + "      assert: rule.result + non_existent_var == true";
+    CelPolicy policy = PARSER.parse(policySource);
+
+    assertThrows(CelPolicyValidationException.class, () -> VERIFIER.verifyInvariants(policy));
+  }
+
+  @Test
+  public void verifyInvariants_restrictedDestinationsPolicy_verified() throws Exception {
+    Cel extendedCel =
+        CEL.toCelBuilder()
+            .addVar("origin", SimpleType.DYN)
+            .addVar("destination", SimpleType.DYN)
+            .addVar("spec", SimpleType.DYN)
+            .addVar("resource", SimpleType.DYN)
+            .addFunctionDeclarations(
+                CelFunctionDecl.newFunctionDeclaration(
+                    "locationCode",
+                    CelOverloadDecl.newGlobalOverload(
+                        "locationCode_string", SimpleType.STRING, SimpleType.STRING)))
+            .build();
+    CelPolicyVerifier verifier =
+        CelPolicyVerifierFactory.newVerifier(
+                CelPolicyCompilerFactory.newPolicyCompiler(extendedCel).build(), AST_VERIFIER)
+            .build();
+
+    CelPolicy policy =
+        PARSER.parse(
+            VerifierTestHelper.loadVerificationPolicyYaml("restricted_destinations_policy.yaml"));
+
+    ImmutableMap<String, CelVerificationResult> results = verifier.verifyInvariants(policy);
+
+    assertThat(results)
+        .containsExactly(
+            "restricted_by_nationality_prohibited", CelVerificationResult.verified(),
+            "restricted_by_origin_ip_prohibited", CelVerificationResult.verified(),
+            "unrestricted_destination_allowed", CelVerificationResult.verified());
+  }
+
+  @Test
+  public void verifyInvariants_invariantReferencesPolicyVariable_verified() throws Exception {
+    String policySource =
+        "name: variable_reference_policy\n" //
+            + "rule:\n" //
+            + "  variables:\n" //
+            + "    - is_admin: role == 'admin'\n" //
+            + "  match:\n" //
+            + "    - condition: variables.is_admin\n" //
+            + "      output: 'true'\n" //
+            + "    - output: 'false'\n" //
+            + "verification:\n" //
+            + "  invariants:\n" //
+            + "    - id: admin_always_true\n" //
+            + "      assume: variables.is_admin\n" //
+            + "      assert: rule.result == true";
+    CelPolicy policy = PARSER.parse(policySource);
+
+    ImmutableMap<String, CelVerificationResult> results = VERIFIER.verifyInvariants(policy);
+
+    assertThat(results).containsKey("admin_always_true");
+    assertThat(results.get("admin_always_true").status()).isEqualTo(VerificationStatus.VERIFIED);
+  }
+
+  @Test
+  public void verifyInvariants_verificationVariablesAndMultiClauseLists_verified()
+      throws Exception {
+    String policySource =
+        "name: verification_ergonomics_policy\n" //
+            + "rule:\n" //
+            + "  variables:\n" //
+            + "    - rule_admin: role == 'admin'\n" //
+            + "  match:\n" //
+            + "    - condition: variables.rule_admin\n" //
+            + "      output: 'true'\n" //
+            + "    - output: 'false'\n" //
+            + "verification:\n" //
+            + "  variables:\n" //
+            + "    - ver_admin: variables.rule_admin && true\n" //
+            + "  invariants:\n" //
+            + "    - id: ergonomic_inv\n" //
+            + "      assume:\n" //
+            + "        - variables.ver_admin\n" //
+            + "        - role != 'editor'\n" //
+            + "      assert:\n" //
+            + "        - rule.result == true\n" //
+            + "        - role == 'admin'";
+    CelPolicy policy = PARSER.parse(policySource);
+
+    ImmutableMap<String, CelVerificationResult> results = VERIFIER.verifyInvariants(policy);
+
+    assertThat(results).containsExactly("ergonomic_inv", CelVerificationResult.verified());
+  }
+
+  @Test
+  public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws Exception {
+    Cel extendedCel =
+        CEL.toCelBuilder()
+            .addVar("is_admin", SimpleType.BOOL)
+            .addVar("is_owner", SimpleType.BOOL)
+            .addVar("is_privileged", SimpleType.BOOL)
+            .addVar("is_prod", SimpleType.BOOL)
+            .addVar("has_approval", SimpleType.BOOL)
+            .addVar("spec", SimpleType.DYN)
+            .build();
+    CelPolicyVerifier verifier =
+        CelPolicyVerifierFactory.newVerifier(
+                CelPolicyCompilerFactory.newPolicyCompiler(extendedCel).build(), AST_VERIFIER)
+            .build();
+
+    CelPolicy policy =
+        PARSER.parse(
+            VerifierTestHelper.loadVerificationPolicyYaml("workload_admission_flawed.yaml"));
+
+    ImmutableMap<String, CelVerificationResult> results = verifier.verifyInvariants(policy);
+
+    assertThat(results).containsKey("universal_no_unapproved_privileged_prod");
+    assertThat(results.get("universal_no_unapproved_privileged_prod").status())
+        .isEqualTo(VerificationStatus.VIOLATED);
+    assertThat(results.get("universal_no_unapproved_privileged_prod").message())
+        .isEqualTo(
+            "Implication violation detected. Counterexample input:\n"
+                + "  is_owner = false\n"
+                + "  is_privileged = true\n"
+                + "  is_prod = true\n"
+                + "  has_approval = false\n"
+                + "  is_admin = true");
+  }
+
+  @Test
+  public void verifyInvariants_workloadAdmissionFixed_verified() throws Exception {
+    Cel extendedCel =
+        CEL.toCelBuilder()
+            .addVar("is_admin", SimpleType.BOOL)
+            .addVar("is_owner", SimpleType.BOOL)
+            .addVar("is_privileged", SimpleType.BOOL)
+            .addVar("is_prod", SimpleType.BOOL)
+            .addVar("has_approval", SimpleType.BOOL)
+            .addVar("spec", SimpleType.DYN)
+            .build();
+    CelPolicyVerifier verifier =
+        CelPolicyVerifierFactory.newVerifier(
+                CelPolicyCompilerFactory.newPolicyCompiler(extendedCel).build(), AST_VERIFIER)
+            .build();
+
+    CelPolicy policy =
+        PARSER.parse(
+            VerifierTestHelper.loadVerificationPolicyYaml("workload_admission_fixed.yaml"));
+
+    ImmutableMap<String, CelVerificationResult> results = verifier.verifyInvariants(policy);
+
+    assertThat(results).containsKey("universal_no_unapproved_privileged_prod");
+    assertWithMessage(results.get("universal_no_unapproved_privileged_prod").message())
+        .that(results.get("universal_no_unapproved_privileged_prod").status())
+        .isEqualTo(VerificationStatus.VERIFIED);
+  }
+
+  @Test
+  public void verifyInvariants_invariantSyntaxError_formatsSnippetAndDescription() throws Exception {
+    String yamlPolicy =
+        "name: syntax_error_policy\n"
+            + "rule:\n"
+            + "  match:\n"
+            + "    - output: 'true'\n"
+            + "verification:\n"
+            + "  invariants:\n"
+            + "    - id: bad_invariant\n"
+            + "      assume:\n"
+            + "        - 'port == 80 &&+ port == 90'\n"
+            + "      assert:\n"
+            + "        - 'rule.result == false'\n";
+    CelPolicy policy = PARSER.parse(yamlPolicy);
+
+    CelPolicyValidationException e =
+        assertThrows(CelPolicyValidationException.class, () -> VERIFIER.verifyInvariants(policy));
+    assertThat(e)
+        .hasMessageThat()
+        .isEqualTo(
+            "ERROR: invariant.bad_invariant.assume:1:14: extraneous input '+' expecting {'[',"
+                + " '{', '(', '.', '-', '!', 'true', 'false', 'null', NUM_FLOAT, NUM_INT,"
+                + " NUM_UINT, STRING, BYTES, IDENTIFIER}\n"
+                + " | port == 80 &&+ port == 90\n"
+                + " | .............^");
+  }
+
+  @Test
+  public void verifyInvariants_verificationVariableSyntaxError_formatsSnippetAndDescription()
+      throws Exception {
+    String yamlPolicy =
+        "name: syntax_error_policy\n"
+            + "rule:\n"
+            + "  match:\n"
+            + "    - output: 'true'\n"
+            + "verification:\n"
+            + "  variables:\n"
+            + "    - bad_var: 'port == 80 &&+ port == 90'\n"
+            + "  invariants:\n"
+            + "    - id: always_secure\n"
+            + "      assert:\n"
+            + "        - 'rule.result == false'\n";
+    CelPolicy policy = PARSER.parse(yamlPolicy);
+
+    CelPolicyValidationException e =
+        assertThrows(CelPolicyValidationException.class, () -> VERIFIER.verifyInvariants(policy));
+    assertThat(e)
+        .hasMessageThat()
+        .isEqualTo(
+            "ERROR: verification.variables.bad_var:1:14: extraneous input '+' expecting {'[',"
+                + " '{', '(', '.', '-', '!', 'true', 'false', 'null', NUM_FLOAT, NUM_INT,"
+                + " NUM_UINT, STRING, BYTES, IDENTIFIER}\n"
+                + " | port == 80 &&+ port == 90\n"
+                + " | .............^");
+  }
+
+  @Test
+  public void verifyInvariants_unrelatedBoundedSymbolApproximate_doesNotForceInconclusive()
+      throws Exception {
+    String yamlPolicy =
+        "name: unrelated_approx_policy\n"
+            + "rule:\n"
+            + "  variables:\n"
+            + "    - unrelated_approx: 'request.matches(\"a\") == true'\n"
+            + "  match:\n"
+            + "    - condition: 'port == 80'\n"
+            + "      output: 'true'\n"
+            + "    - output: 'false'\n"
+            + "verification:\n"
+            + "  invariants:\n"
+            + "    - id: port_check\n"
+            + "      assume:\n"
+            + "        - 'port == 80'\n"
+            + "      assert:\n"
+            + "        - 'rule.result == true'\n";
+    CelPolicy policy = PARSER.parse(yamlPolicy);
+
+    ImmutableMap<String, CelVerificationResult> results = VERIFIER.verifyInvariants(policy);
+
+    assertThat(results).containsKey("port_check");
+    assertThat(results.get("port_check").status()).isEqualTo(VerificationStatus.VERIFIED);
+  }
+
+  @Test
+  public void verifyInvariants_verificationVariablesCanReferenceRuleResult() throws Exception {
+    String yamlPolicy =
+        "name: rule_result_in_ver_var_policy\n"
+            + "rule:\n"
+            + "  match:\n"
+            + "    - condition: 'port == 80'\n"
+            + "      output: 'true'\n"
+            + "    - output: 'false'\n"
+            + "verification:\n"
+            + "  variables:\n"
+            + "    - is_denied: 'rule.result == false'\n"
+            + "  invariants:\n"
+            + "    - id: port_check\n"
+            + "      assume:\n"
+            + "        - 'port == 80'\n"
+            + "      assert:\n"
+            + "        - 'variables.is_denied == false'\n";
+    CelPolicy policy = PARSER.parse(yamlPolicy);
+
+    ImmutableMap<String, CelVerificationResult> results = VERIFIER.verifyInvariants(policy);
+
+    assertThat(results).containsKey("port_check");
+    assertThat(results.get("port_check").status()).isEqualTo(VerificationStatus.VERIFIED);
+  }
+
+  @Test
+  public void verifyInvariants_boundedSymbolWithApproximation_returnsInconclusive()
+      throws Exception {
+    String yamlPolicy =
+        "name: approx_symbol_policy\n"
+            + "rule:\n"
+            + "  variables:\n"
+            + "    - approx_var: 'request.matches(\"^[a-z]+$\") == true'\n"
+            + "  match:\n"
+            + "    - condition: 'variables.approx_var'\n"
+            + "      output: 'true'\n"
+            + "    - output: 'false'\n"
+            + "verification:\n"
+            + "  invariants:\n"
+            + "    - id: check_approx\n"
+            + "      assert:\n"
+            + "        - 'variables.approx_var == true'\n";
+    CelPolicy policy = PARSER.parse(yamlPolicy);
+
+    ImmutableMap<String, CelVerificationResult> results = VERIFIER.verifyInvariants(policy);
+
+    assertThat(results).containsKey("check_approx");
+    assertThat(results.get("check_approx").status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
+  }
 }
diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
index 6d046b6b9..4ab1d050f 100644
--- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
+++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
@@ -20,6 +20,7 @@
 import static org.junit.Assert.assertThrows;
 
 import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.ImmutableSet;
 import com.google.testing.junit.testparameterinjector.TestParameter;
 import com.google.testing.junit.testparameterinjector.TestParameterInjector;
@@ -2454,4 +2455,21 @@ public void verifyEquivalence_timeoutReached_throwsCelVerificationException() th
             CelVerificationException.class, () -> timeoutVerifier.verifyEquivalence(astA, astB));
     assertThat(e).hasMessageThat().containsMatch("timeout|canceled");
   }
+
+  @Test
+  public void verifyImplication_loopExceedsLimit_returnsTruncatedInconclusive() throws Exception {
+    CelAbstractSyntaxTree assumeAst =
+        CEL.compile("size(int_list) <= 2 && int_list[0] > 0 && int_list[1] > 0").getAst();
+    CelAbstractSyntaxTree assertAst = CEL.compile("int_list.all(x, x > 0)").getAst();
+
+    CelVerifier verifier =
+        CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(2).build();
+    CelVerificationResult result =
+        ((CelVerifierZ3Impl) verifier)
+            .verifyImplication(assumeAst, assertAst, ImmutableMap.of());
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
+    assertThat(result.message())
+        .contains("implication holds within the current loop unroll limit");
+  }
 }
diff --git a/verifier/src/test/java/dev/cel/verifier/VerifierTestHelper.java b/verifier/src/test/java/dev/cel/verifier/VerifierTestHelper.java
new file mode 100644
index 000000000..b54d01d44
--- /dev/null
+++ b/verifier/src/test/java/dev/cel/verifier/VerifierTestHelper.java
@@ -0,0 +1,58 @@
+// Copyright 2026 Google LLC
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//      https://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package dev.cel.verifier;
+
+import static java.nio.charset.StandardCharsets.UTF_8;
+
+import com.google.common.base.Ascii;
+import com.google.common.io.Files;
+import com.google.devtools.build.runfiles.AutoBazelRepository;
+import com.google.devtools.build.runfiles.Runfiles;
+import java.io.File;
+import java.io.IOException;
+
+/** Package-private class to assist with verifier testing and runfiles resolution. */
+@AutoBazelRepository
+final class VerifierTestHelper {
+
+  private static final Runfiles runfiles = createRunfiles();
+
+  static String loadVerificationPolicyYaml(String filename) throws IOException {
+    String rlocationPath =
+        "cel_java/testing/src/test/resources/policy/verification/" + filename;
+    String resolvedPath = runfiles.rlocation(Ascii.toLowerCase(rlocationPath));
+    if (resolvedPath == null) {
+      throw new IOException("Unmapped runfile path: " + rlocationPath);
+    }
+    File file = new File(resolvedPath);
+    if (!file.exists()) {
+      throw new IOException(
+          String.format(
+              "Runfile not found on disk at '%s' (unresolved path: '%s')",
+              resolvedPath, rlocationPath));
+    }
+    return Files.asCharSource(file, UTF_8).read();
+  }
+
+  private static Runfiles createRunfiles() {
+    try {
+      return Runfiles.preload().withSourceRepository(AutoBazelRepository_VerifierTestHelper.NAME);
+    } catch (IOException e) {
+      throw new RuntimeException("Failed to initialize Runfiles", e);
+    }
+  }
+
+  private VerifierTestHelper() {}
+}