cel-expr · copybara-service · Aug 15, 2026
diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel
@@ -11,6 +11,7 @@ package(
 java_library(
     name = "verifier",
     srcs = [
+        "CelCounterexample.java",
         "CelVerificationException.java",
         "CelVerificationResult.java",
         "CelVerifier.java",
@@ -23,6 +24,8 @@ java_library(
         "//common:cel_ast",
         "//common/types:type_providers",
         "@maven//:com_google_errorprone_error_prone_annotations",
+        "@maven//:com_google_guava_guava",
+        "@maven//:org_jspecify_jspecify",
     ],
 )
 
@@ -153,6 +156,7 @@ java_library(
 java_library(
     name = "z3_impl",
     srcs = [
+        "CegarRefiner.java",
         "CelAstAlphaHasher.java",
         "CelAstToZ3Translator.java",
         "CelVerifierZ3Impl.java",
@@ -180,9 +184,12 @@ java_library(
         "//common/types",
         "//common/types:cel_types",
         "//common/types:type_providers",
+        "//common/values:cel_byte_string",
+        "//common/values:cel_value_provider",
         "//optimizer",
         "//optimizer:optimization_exception",
         "//optimizer:optimizer_builder",
+        "//runtime:evaluation_exception",
         "//verifier/axioms",
         "@maven//:com_google_errorprone_error_prone_annotations",
         "@maven//:com_google_guava_guava",

diff --git a/verifier/src/main/java/dev/cel/verifier/CegarRefiner.java b/verifier/src/main/java/dev/cel/verifier/CegarRefiner.java
@@ -0,0 +1,137 @@
+// 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 com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableMap;
+import com.google.errorprone.annotations.Immutable;
+import dev.cel.bundle.Cel;
+import dev.cel.common.CelAbstractSyntaxTree;
+import dev.cel.runtime.CelEvaluationException;
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Objects;
+import java.util.Optional;
+
+/**
+ * Evaluates candidate counterexample models against the concrete CEL runtime to confirm or refute
+ * potential violations (CEGAR refinement loop).
+ */
+@Immutable
+final class CegarRefiner {
+
+  @Immutable
+  static final class CegarOutcome {
+    private final boolean isViolation;
+    private final Optional<String> evaluationErrorMessage;
+
+    static CegarOutcome violation() {
+      return new CegarOutcome(true, Optional.empty());
+    }
+
+    static CegarOutcome spurious() {
+      return new CegarOutcome(false, Optional.empty());
+    }
+
+    static CegarOutcome evaluationError(String errorMessage) {
+      return new CegarOutcome(false, Optional.of(errorMessage));
+    }
+
+    private CegarOutcome(boolean isViolation, Optional<String> evaluationErrorMessage) {
+      this.isViolation = isViolation;
+      this.evaluationErrorMessage = evaluationErrorMessage;
+    }
+
+    boolean isViolation() {
+      return isViolation;
+    }
+
+    Optional<String> evaluationErrorMessage() {
+      return evaluationErrorMessage;
+    }
+  }
+
+  private final Cel cel;
+
+  CegarRefiner(Cel cel) {
+    this.cel = Preconditions.checkNotNull(cel);
+  }
+
+  CegarOutcome refineEquivalence(
+      CelAbstractSyntaxTree astA, CelAbstractSyntaxTree astB, CelCounterexample model) {
+    if (model.isSatisfyingInput()) {
+      return CegarOutcome.spurious();
+    }
+    try {
+      ImmutableMap<String, Object> evalContext = model.toEvaluationContext();
+      Object resA = cel.createProgram(astA).eval(evalContext);
+      Object resB = cel.createProgram(astB).eval(evalContext);
+      // If concrete evaluation produces identical results, the candidate SMT divergence was an
+      // artifact of abstraction (spurious). Otherwise, concrete outputs diverge (violation).
+      return Objects.equals(resA, resB) ? CegarOutcome.spurious() : CegarOutcome.violation();
+    } catch (CelEvaluationException e) {
+      return CegarOutcome.evaluationError(e.getMessage());
+    }
+  }
+
+  CegarOutcome refineSatisfiability(
+      CelAbstractSyntaxTree ast, boolean searchForCounterexample, CelCounterexample model) {
+    if (searchForCounterexample ? model.isSatisfyingInput() : !model.isSatisfyingInput()) {
+      return CegarOutcome.spurious();
+    }
+    try {
+      ImmutableMap<String, Object> evalContext = model.toEvaluationContext();
+      Object res = cel.createProgram(ast).eval(evalContext);
+      boolean isEvaluationTrue = Objects.equals(res, true);
+      // For universal truth (searchForCounterexample=true), evaluating to true refutes the
+      // candidate counterexample (spurious). For satisfiability search
+      // (searchForCounterexample=false),
+      // evaluating to true confirms the candidate satisfying model (violation).
+      boolean isSpurious = searchForCounterexample == isEvaluationTrue;
+      return isSpurious ? CegarOutcome.spurious() : CegarOutcome.violation();
+    } catch (CelEvaluationException e) {
+      return CegarOutcome.evaluationError(e.getMessage());
+    }
+  }
+
+  CegarOutcome refineImplication(
+      CelAbstractSyntaxTree assumeAst,
+      CelAbstractSyntaxTree assertAst,
+      Map<String, CelAbstractSyntaxTree> boundSymbols,
+      CelCounterexample model) {
+    if (model.isSatisfyingInput()) {
+      return CegarOutcome.spurious();
+    }
+    try {
+      Map<String, Object> evalContext = new HashMap<>(model.toEvaluationContext());
+      for (Map.Entry<String, CelAbstractSyntaxTree> entry : boundSymbols.entrySet()) {
+        Object boundVal = cel.createProgram(entry.getValue()).eval(evalContext);
+        evalContext.put(entry.getKey(), boundVal);
+      }
+      Object assumeVal = cel.createProgram(assumeAst).eval(evalContext);
+      if (Objects.equals(assumeVal, true)) {
+        Object assertVal = cel.createProgram(assertAst).eval(evalContext);
+        // If the premise holds and the conclusion evaluates to true, the candidate counterexample
+        // is refuted (spurious). If the conclusion fails under true premise, implication is
+        // violated.
+        return Objects.equals(assertVal, true) ? CegarOutcome.spurious() : CegarOutcome.violation();
+      }
+      // The candidate input did not satisfy the premise, so it cannot serve as a counterexample.
+      return CegarOutcome.spurious();
+    } catch (CelEvaluationException e) {
+      return CegarOutcome.evaluationError(e.getMessage());
+    }
+  }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
@@ -610,7 +610,7 @@ private FieldAccess getMapAccess(Expr<?> operand, String field, BoolExpr typeGua
     typeConstraints.add(
         ctx.mkImplies(
             CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotError));
-    if (unknownIdentifiers.isEmpty()) {
+    if (!unknownIdentifiers.contains(field)) {
       BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(value));
       typeConstraints.add(
           ctx.mkImplies(
@@ -630,7 +630,7 @@ private FieldAccess getMsgAccess(Expr<?> operand, String field, BoolExpr typeGua
     typeConstraints.add(
         ctx.mkImplies(
             CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotError));
-    if (unknownIdentifiers.isEmpty()) {
+    if (!unknownIdentifiers.contains(field)) {
       BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(value));
       typeConstraints.add(
           ctx.mkImplies(

diff --git a/verifier/src/main/java/dev/cel/verifier/CelCounterexample.java b/verifier/src/main/java/dev/cel/verifier/CelCounterexample.java
@@ -0,0 +1,99 @@
+// 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 com.google.auto.value.AutoValue;
+import com.google.common.collect.ImmutableMap;
+import com.google.errorprone.annotations.Immutable;
+import dev.cel.common.types.CelType;
+import java.util.Map;
+import java.util.Optional;
+import org.jspecify.annotations.Nullable;
+
+/** Encapsulates a structured variable assignment model produced by formal verification. */
+@AutoValue
+@AutoValue.CopyAnnotations
+@Immutable
+public abstract class CelCounterexample {
+
+  /** Represents a single variable binding within a counterexample. */
+  @AutoValue
+  @AutoValue.CopyAnnotations
+  @Immutable
+  @SuppressWarnings("Immutable") // Values are deeply immutable.
+  public abstract static class Binding {
+    /** Returns the name of the variable. */
+    public abstract String name();
+
+    /** Returns the inferred CEL type of the variable. */
+    public abstract CelType type();
+
+    /**
+     * Returns the native Java representation of the value (e.g., Long, Boolean, String, Instant,
+     * Duration, ImmutableList, ImmutableMap, Message, etc.), or empty if unassigned or unavailable.
+     */
+    public abstract Optional<Object> nativeValue();
+
+    /**
+     * Returns the CEL literal representation of the value (e.g., "80", "\"admin\"", "true", "[1,
+     * 2]").
+     */
+    public abstract String celString();
+
+    public static Binding of(
+        String name, CelType type, @Nullable Object nativeValue, String celString) {
+      return new AutoValue_CelCounterexample_Binding(
+          name, type, Optional.ofNullable(nativeValue), celString);
+    }
+  }
+
+  /** Returns all variable bindings keyed by variable name. */
+  public abstract ImmutableMap<String, Binding> bindings();
+
+  /** Returns true if this counterexample was derived from an approximate solver model. */
+  public abstract boolean isApproximate();
+
+  /** Returns true if this model represents a satisfying assignment rather than a counterexample. */
+  public abstract boolean isSatisfyingInput();
+
+  /** Returns the formatted display string representation. */
+  public abstract String toDisplayString();
+
+  /** Looks up a variable binding by name. */
+  public Optional<Binding> get(String variableName) {
+    return Optional.ofNullable(bindings().get(variableName));
+  }
+
+  /**
+   * Returns a native Java variable map suitable for evaluating expressions in CelRuntime (e.g.,
+   * Cel.createProgram().eval(toEvaluationContext())).
+   */
+  public ImmutableMap<String, Object> toEvaluationContext() {
+    ImmutableMap.Builder<String, Object> builder = ImmutableMap.builder();
+    for (Binding binding : bindings().values()) {
+      binding.nativeValue().ifPresent(value -> builder.put(binding.name(), value));
+    }
+    return builder.buildOrThrow();
+  }
+
+  public static CelCounterexample create(
+      Map<String, Binding> bindings,
+      boolean isApproximate,
+      boolean isSatisfyingInput,
+      String toDisplayString) {
+    return new AutoValue_CelCounterexample(
+        ImmutableMap.copyOf(bindings), isApproximate, isSatisfyingInput, toDisplayString);
+  }
+}
diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java b/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java
@@ -15,9 +15,12 @@
 package dev.cel.verifier;
 
 import com.google.auto.value.AutoValue;
+import com.google.errorprone.annotations.Immutable;
+import java.util.Optional;
 
 /** Result object containing the outcome of a CEL AST verification check. */
 @AutoValue
+@Immutable
 public abstract class CelVerificationResult {
 
   /** Represents the outcome of the verification process. */
@@ -38,11 +41,12 @@ public enum VerificationStatus {
    */
   public abstract String reason();
 
-  /**
-   * Returns a detailed counterexample or satisfying model assignment, if one was found.
-   */
+  /** Returns a detailed counterexample or satisfying model assignment string, if one was found. */
   public abstract String counterexample();
 
+  /** Returns the structured counterexample or satisfying model assignment, if one was found. */
+  public abstract Optional<CelCounterexample> counterexampleModel();
+
   /**
    * Returns a message detailing the outcome of the verification check, such as a counterexample
    * input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED
@@ -53,28 +57,41 @@ public String message() {
   }
 
   static CelVerificationResult verified() {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", "");
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.VERIFIED, "", "", Optional.empty());
   }
 
-  static CelVerificationResult verified(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, "");
+  static CelVerificationResult verified(String reason, CelCounterexample counterexample) {
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.VERIFIED,
+        reason,
+        counterexample.toDisplayString(),
+        Optional.of(counterexample));
   }
 
   static CelVerificationResult failed(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, "");
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.VIOLATED, reason, "", Optional.empty());
   }
 
-  static CelVerificationResult failed(String reason, String counterexample) {
+  static CelVerificationResult failed(String reason, CelCounterexample counterexample) {
     return new AutoValue_CelVerificationResult(
-        VerificationStatus.VIOLATED, reason, counterexample);
+        VerificationStatus.VIOLATED,
+        reason,
+        counterexample.toDisplayString(),
+        Optional.of(counterexample));
   }
 
   static CelVerificationResult inconclusive(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, "");
+    return new AutoValue_CelVerificationResult(
+        VerificationStatus.INCONCLUSIVE, reason, "", Optional.empty());
   }
 
-  static CelVerificationResult inconclusive(String reason, String counterexample) {
+  static CelVerificationResult inconclusive(String reason, CelCounterexample counterexample) {
     return new AutoValue_CelVerificationResult(
-        VerificationStatus.INCONCLUSIVE, reason, counterexample);
+        VerificationStatus.INCONCLUSIVE,
+        reason,
+        counterexample.toDisplayString(),
+        Optional.of(counterexample));
   }
 }
diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierBuilder.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierBuilder.java
@@ -82,6 +82,23 @@ public interface CelVerifierBuilder {
   @CanIgnoreReturnValue
   CelVerifierBuilder setComprehensionUnrollLimit(int unrollLimit);
 
+  /**
+   * Enables or disables Counterexample-Guided Abstraction Refinement (CEGAR).
+   *
+   * <p>When enabled, if the SMT solver returns an approximate model (e.g., due to unmodeled custom
+   * functions, approximations, or bounded loops), the candidate inputs are validated using concrete
+   * {@link dev.cel.bundle.Cel} program execution. If concrete evaluation confirms an invariant
+   * violation or equivalence divergence, the result is upgraded from {@code INCONCLUSIVE} to {@code
+   * VIOLATED}.
+   *
+   * <p><strong>Note:</strong> This option requires an execution-ready CEL environment where any
+   * custom functions referenced in the policy have registered runtime {@link
+   * dev.cel.runtime.CelFunctionBinding} implementations. In declaration-only environments (e.g.,
+   * static linters without runtime bindings), this should remain disabled.
+   */
+  @CanIgnoreReturnValue
+  CelVerifierBuilder setEnableCegarRefinement(boolean enableCegarRefinement);
+
   /** Builds the {@link CelVerifier} instance. */
   CelVerifier build();
 }