Introduce cel_verifier_test Bazel macro for CEL verification.

verifier/tools/BUILD.bazel

@@ -1,8 +1,13 @@
+load("@bazel_skylib//:bzl_library.bzl", "bzl_library")
+load(":cel_verifier.bzl", "cel_verifier_test")
+
 package(
     default_applicable_licenses = ["//:license"],
     default_visibility = ["//verifier:verifier_internal"],
 )
 
+exports_files(["run_verifier.sh"])
+
 alias(
     name = "tools",
     actual = "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib",
@@ -17,3 +22,60 @@ alias(
     name = "cel_verifier_tool",
     actual = "//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool",
 )
+
+cel_verifier_test(
+    name = "test_sat_simple_test",
+    command = "check-sat",
+    expected_status = [
+        "VERIFIED",
+        "INCONCLUSIVE",
+    ],  # Pass if verified OR inconclusive
+    expression = "x > 10",
+    variables = {"x": "int"},
+)
+
+cel_verifier_test(
+    name = "test_sat_unsatisfiable_test",
+    command = "check-sat",
+    expected_status = ["VIOLATED"],
+    expression = "x > 10 && x < 5",
+    variables = {"x": "int"},
+)
+
+cel_verifier_test(
+    name = "test_equiv_simple_test",
+    command = "verify-equiv",
+    expression = "x > 10",
+    expression_b = "10 < x",
+    variables = {"x": "int"},
+)
+
+cel_verifier_test(
+    name = "test_policy_simple_test",
+    command = "verify-policy",
+    policy_file = "testdata/simple_policy.yaml",
+    variables = {"role": "string"},
+)
+
+cel_verifier_test(
+    name = "test_equiv_negative_test",
+    command = "verify-equiv",
+    expected_status = ["VIOLATED"],
+    expression = "x > 10",
+    expression_b = "x < 5",
+    variables = {"x": "int"},
+)
+
+cel_verifier_test(
+    name = "test_policy_violated_test",
+    command = "verify-policy",
+    expected_status = ["VIOLATED"],
+    policy_file = "testdata/violated_policy.yaml",
+    variables = {"role": "string"},
+)
+
+bzl_library(
+    name = "cel_verifier_bzl",
+    srcs = ["cel_verifier.bzl"],
+    visibility = ["//visibility:private"],
+)

verifier/tools/cel_verifier.bzl

@@ -0,0 +1,154 @@
+# 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.
+
+"""Macros for CEL Formal Verifier."""
+
+load("@rules_shell//shell:sh_test.bzl", "sh_test")
+load("@bazel_skylib//lib:shell.bzl", "shell")
+
+# Mapping of friendly status names to CelVerifierTool exit codes
+_STATUS_TO_EXIT_CODE = {
+    "VERIFIED": "0",
+    "VIOLATED": "1",
+    "INCONCLUSIVE": "2",
+    "ERROR": "3",
+}
+
+def _make_verifier_args(
+        command,
+        expression = None,
+        expression_b = None,
+        policy_file = None,
+        variables = {},
+        unknowns = [],
+        timeout = 10,
+        unroll_limit = 5):
+    args = []
+    srcs = []
+
+    if command not in ["check-sat", "check-valid", "verify-equiv", "verify-policy"]:
+        fail("Unsupported command: " + command)
+
+    args.append(command)
+
+    if command in ["check-sat", "check-valid"]:
+        if not expression:
+            fail("expression is required for " + command)
+        args.append("--expr")
+        args.append(expression)
+    elif command == "verify-equiv":
+        if not expression or not expression_b:
+            fail("expression and expression_b are required for verify-equiv")
+        args.append("--expr1")
+        args.append(expression)
+        args.append("--expr2")
+        args.append(expression_b)
+    elif command == "verify-policy":
+        if not policy_file:
+            fail("policy_file is required for verify-policy")
+        args.append("--file")
+        args.append("$(rootpath %s)" % policy_file)
+        srcs.append(policy_file)
+
+    for var_name, var_type in variables.items():
+        args.append("--var")
+        args.append("%s:%s" % (var_name, var_type))
+
+    for unknown in unknowns:
+        args.append("--unknown")
+        args.append(unknown)
+
+    args.append("--timeout")
+    args.append(str(timeout))
+
+    args.append("--unroll-limit")
+    args.append(str(unroll_limit))
+
+    args.append("--output_format")
+    args.append("TEXT")
+
+    return args, srcs
+
+def cel_verifier_test(
+        name,
+        command,
+        expression = None,
+        expression_b = None,
+        policy_file = None,
+        variables = {},
+        unknowns = [],
+        timeout = 10,
+        unroll_limit = 5,
+        expected_status = ["VERIFIED"],
+        **kwargs):
+    """Verifies a CEL expression or policy via a test rule.
+
+    See //verifier/tools/README.md for more details on CLI commands and options.
+
+    Args:
+      name: str name for the test
+      command: str verification command. Supported commands:
+        - 'check-sat': Verify satisfiability of a CEL expression & generate witness model.
+        - 'check-valid': Verify validity (isAlwaysTrue) of a CEL expression & generate counterexample.
+        - 'verify-equiv': Prove logical equivalence between two CEL expressions.
+        - 'verify-policy': Verify policy invariants defined in a YAML policy file.
+      expression: str CEL expression to verify (required for check-sat, check-valid, verify-equiv)
+      expression_b: str second CEL expression for equivalence check (required for verify-equiv)
+      policy_file: label of a YAML policy file to verify (required for verify-policy)
+      variables: dict of var_name -> type_string (e.g., {"port": "int"})
+      unknowns: list of str unknown identifiers
+      timeout: int solver timeout in seconds (default 10)
+      unroll_limit: int comprehension unroll limit (default 5)
+      expected_status: list of str expected verification statuses (default ["VERIFIED"]).
+        Supported statuses: 'VERIFIED', 'VIOLATED', 'INCONCLUSIVE', 'ERROR'.
+      **kwargs: other standard Bazel attributes
+    """
+
+    args, srcs = _make_verifier_args(
+        command = command,
+        expression = expression,
+        expression_b = expression_b,
+        policy_file = policy_file,
+        variables = variables,
+        unknowns = unknowns,
+        timeout = timeout,
+        unroll_limit = unroll_limit,
+    )
+
+    tags = kwargs.pop("tags", [])
+    if "nomsan" not in tags:
+        tags = tags + ["nomsan"]
+
+    allowed_codes = []
+    for status in expected_status:
+        if status not in _STATUS_TO_EXIT_CODE:
+            fail("Unsupported status in expected_status: " + status)
+        allowed_codes.append(_STATUS_TO_EXIT_CODE[status])
+
+    allowed_codes_str = ",".join(allowed_codes)
+
+    env = kwargs.pop("env", {})
+    env["ALLOWED_EXIT_CODES"] = allowed_codes_str
+
+    sh_test(
+        name = name,
+        srcs = ["//verifier/tools:run_verifier.sh"],
+        args = [shell.quote("$(rootpath //verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool)")] + [shell.quote(a) for a in args],
+        data = [
+            "//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool",
+        ] + srcs,
+        tags = tags,
+        env = env,
+        **kwargs
+    )

verifier/tools/run_verifier.sh

@@ -0,0 +1,35 @@
+#!/bin/bash
+# Path: //third_party/java/cel/verifier/tools/run_verifier.sh
+#
+# This script is used by the cel_verifier_test macro to invoke the
+# underlying Java binary (CelVerifierTool) with the arguments passed to the macro.
+# It uses 'find' to locate the binary in the runfiles directory, which works
+# in both Google3 and Bazel environments.
+
+die() {
+  echo "ERROR: $*" >&2
+  exit 1
+}
+
+if [ -z "$1" ]; then
+  die "Verifier binary path not provided as first argument."
+fi
+
+VERIFIER_BINARY="$1"
+shift
+
+# Execute the verifier binary with all passed arguments.
+"$VERIFIER_BINARY" "$@"
+ACTUAL_EXIT_CODE=$?
+
+# Default to expecting 0 (VERIFIED) if env is not set
+ALLOWED_CODES=${ALLOWED_EXIT_CODES:-"0"}
+
+# Check if the actual exit code is in the allowed list
+if [[ ",$ALLOWED_CODES," =~ ",$ACTUAL_EXIT_CODE," ]]; then
+  echo "Verification finished with status code $ACTUAL_EXIT_CODE (Allowed: $ALLOWED_CODES)"
+  exit 0
+else
+  echo "ERROR: Verification finished with unexpected status code $ACTUAL_EXIT_CODE (Allowed: $ALLOWED_CODES)" >&2
+  exit 1
+fi

verifier/tools/testdata/simple_policy.yaml

@@ -0,0 +1,11 @@
+name: simple_policy
+rule:
+  match:
+    - condition: role == 'admin'
+      output: 'true'
+    - output: 'false'
+verification:
+  invariants:
+    - id: admin_always_true
+      assume: role == 'admin'
+      assert: rule.result == true

verifier/tools/testdata/violated_policy.yaml

@@ -0,0 +1,11 @@
+name: violated_policy
+rule:
+  match:
+    - condition: role == 'admin'
+      output: 'true'
+    - output: 'false'
+verification:
+  invariants:
+    - id: viewer_always_true
+      assume: role == 'viewer'
+      assert: rule.result == true