Add CLI for Verifier

verifier/README.md

@@ -433,3 +433,7 @@ What this means for verification:
     default unless you have a specific need and bounded inputs.
 
 ---
+
+## Tools & CLI
+
+For command-line verification and interactive execution, see the [CLI Tool documentation](tools/README.md).

verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel

@@ -0,0 +1,77 @@
+load("@rules_java//java:defs.bzl", "java_binary", "java_library")
+load("//publish:cel_version.bzl", "CEL_VERSION")
+
+package(
+    default_applicable_licenses = [
+        "//:license",
+    ],
+    default_visibility = [
+        "//verifier:__subpackages__",
+    ],
+)
+
+genrule(
+    name = "generate_version",
+    outs = ["CelVersion.java"],
+    cmd = """cat << 'EOF' > $@
+package dev.cel.verifier.tools;
+
+final class CelVersion {
+  static final String VERSION = "%s";
+
+  private CelVersion() {}
+}
+EOF
+""" % CEL_VERSION,
+)
+
+java_library(
+    name = "tools_lib",
+    srcs = [
+        "CelVerifierTool.java",
+        "CelVerifierToolCore.java",
+        "FormatUtils.java",
+        "VerificationOptions.java",
+        ":generate_version",
+    ],
+    tags = [
+        "alt_dep=//verifier/tools",
+    ],
+    deps = [
+        "//bundle:cel",
+        "//common:cel_ast",
+        "//common:compiler_common",
+        "//common:options",
+        "//common/types",
+        "//common/types:type_providers",
+        "//compiler",
+        "//compiler:compiler_builder",
+        "//extensions",
+        "//parser:macro",
+        "//policy",
+        "//policy:compiler",
+        "//policy:compiler_factory",
+        "//policy:parser",
+        "//policy:parser_factory",
+        "//policy:validation_exception",
+        "//verifier",
+        "//verifier:policy_verifier",
+        "//verifier:policy_verifier_factory",
+        "//verifier:verifier_factory",
+        "@maven//:com_google_errorprone_error_prone_annotations",
+        "@maven//:com_google_guava_guava",
+        "@maven//:info_picocli_picocli",
+    ],
+)
+
+java_binary(
+    name = "cel_verifier_tool",
+    jvm_flags = ["-Dz3.skipLibraryLoad=true"],
+    main_class = "dev.cel.verifier.tools.CelVerifierTool",
+    tags = [
+        "alt_dep=//verifier/tools:cel_verifier_tool",
+    ],
+    runtime_deps = [
+        ":tools_lib",
+    ],
+)

verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java

@@ -0,0 +1,303 @@
+// 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.tools;
+
+import com.google.common.collect.ImmutableMap;
+import dev.cel.common.CelValidationException;
+import dev.cel.common.types.CelType;
+import dev.cel.policy.CelPolicyValidationException;
+import dev.cel.verifier.CelVerificationResult;
+import dev.cel.verifier.CelVerificationResult.VerificationStatus;
+import dev.cel.verifier.tools.VerificationOptions.OutputFormat;
+import java.io.File;
+import java.io.OutputStreamWriter;
+import java.io.PrintWriter;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.time.Duration;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Locale;
+import java.util.concurrent.Callable;
+import picocli.CommandLine;
+import picocli.CommandLine.Command;
+import picocli.CommandLine.IVersionProvider;
+import picocli.CommandLine.Model.CommandSpec;
+import picocli.CommandLine.Option;
+import picocli.CommandLine.Spec;
+
+/** Main Picocli entrypoint for the CEL Formal Verification CLI. */
+@Command(
+    name = "cel-verifier",
+    mixinStandardHelpOptions = true,
+    versionProvider = CelVerifierTool.VersionProvider.class,
+    description = "CEL-Java Formal Verification CLI Tool",
+    subcommands = {
+      CelVerifierTool.CheckSatCommand.class,
+      CelVerifierTool.CheckValidCommand.class,
+      CelVerifierTool.VerifyEquivCommand.class,
+      CelVerifierTool.VerifyPolicyCommand.class
+    })
+public final class CelVerifierTool implements Runnable {
+
+  static final int EXIT_CODE_VERIFIED = 0;
+  static final int EXIT_CODE_VIOLATED = 1;
+  static final int EXIT_CODE_INCONCLUSIVE = 2;
+  static final int EXIT_CODE_ERROR = 3;
+
+  static final class VersionProvider implements IVersionProvider {
+    @Override
+    public String[] getVersion() {
+      return new String[] {"cel-verifier " + CelVersion.VERSION};
+    }
+  }
+
+  @Spec private CommandSpec spec;
+
+  @Override
+  public void run() {
+    spec.commandLine().usage(spec.commandLine().getOut());
+  }
+
+  /** Options shared across all verification commands. */
+  abstract static class BaseVerificationCommand implements Callable<Integer> {
+
+    @Spec private CommandSpec spec;
+
+    PrintWriter out() {
+      return spec != null
+          ? spec.commandLine().getOut()
+          : new PrintWriter(new OutputStreamWriter(System.out, StandardCharsets.UTF_8), true);
+    }
+
+    PrintWriter err() {
+      return spec != null
+          ? spec.commandLine().getErr()
+          : new PrintWriter(new OutputStreamWriter(System.err, StandardCharsets.UTF_8), true);
+    }
+
+    @Option(
+        names = {"--var", "-v"},
+        description =
+            "Declared variable in 'name:type' format (e.g., --var role:string --var port:int)")
+    List<String> variables = new ArrayList<>();
+
+    @Option(
+        names = {"--unknown", "-u"},
+        description =
+            "Identifier to permit evaluating to Unknown (e.g., --unknown request.headers)")
+    List<String> unknownIdentifiers = new ArrayList<>();
+
+    @Option(
+        names = {"--timeout"},
+        description = "Solver timeout in seconds (default: 10)")
+    int timeoutSeconds = (int) VerificationOptions.DEFAULT_TIMEOUT.getSeconds();
+
+    @Option(
+        names = {"--unroll-limit"},
+        description = "Comprehension unroll limit for BMC (default: 5)")
+    int comprehensionUnrollLimit = VerificationOptions.DEFAULT_COMPREHENSION_UNROLL_LIMIT;
+
+    @Option(
+        names = {"--output_format", "-fmt"},
+        description = "Output format: TEXT or JSON (default: TEXT)")
+    String outputFormatStr = VerificationOptions.DEFAULT_OUTPUT_FORMAT.name();
+
+    @FunctionalInterface
+    protected interface CommandAction {
+      int execute(VerificationOptions options, ImmutableMap<String, CelType> vars) throws Exception;
+    }
+
+    protected int executeCommand(CommandAction action) {
+      return executeCommand("Verification error", action);
+    }
+
+    protected int executeCommand(String errorPrefix, CommandAction action) {
+      try {
+        VerificationOptions options = getOptions();
+        ImmutableMap<String, CelType> vars = VerificationOptions.parseVariables(variables);
+        return action.execute(options, vars);
+      } catch (CelValidationException e) {
+        err().println("Compilation error:\n" + e.getMessage());
+        return EXIT_CODE_ERROR;
+      } catch (CelPolicyValidationException e) {
+        err().println("Policy compilation error:\n" + e.getMessage());
+        return EXIT_CODE_ERROR;
+      } catch (Exception e) {
+        err().println(errorPrefix + ": " + e.getMessage());
+        return EXIT_CODE_ERROR;
+      }
+    }
+
+    protected VerificationOptions getOptions() {
+      OutputFormat format = OutputFormat.TEXT;
+      try {
+        format = OutputFormat.valueOf(outputFormatStr.toUpperCase(Locale.US));
+      } catch (IllegalArgumentException e) {
+        err().println("Invalid output format '" + outputFormatStr + "'. Defaulting to TEXT.");
+      }
+      return VerificationOptions.builder()
+          .setTimeout(Duration.ofSeconds(timeoutSeconds))
+          .setComprehensionUnrollLimit(comprehensionUnrollLimit)
+          .setUnknownIdentifiers(unknownIdentifiers)
+          .setOutputFormat(format)
+          .build();
+    }
+
+    protected int handleSingleResult(CelVerificationResult result, OutputFormat format) {
+      if (format == OutputFormat.JSON) {
+        out().println(FormatUtils.formatJsonResult(result));
+      } else {
+        out().println(FormatUtils.formatTextResult(result));
+      }
+
+      if (result.status() == VerificationStatus.VERIFIED) {
+        return EXIT_CODE_VERIFIED;
+      } else if (result.status() == VerificationStatus.VIOLATED) {
+        return EXIT_CODE_VIOLATED;
+      } else {
+        return EXIT_CODE_INCONCLUSIVE;
+      }
+    }
+  }
+
+  /** Base command for commands operating on a single CEL expression. */
+  abstract static class SingleExpressionCommand extends BaseVerificationCommand {
+    @Option(
+        names = {"--expr", "-e"},
+        required = true,
+        description = "CEL expression string to verify")
+    String expression = "";
+  }
+
+  @Command(
+      name = "check-sat",
+      description = "Verify satisfiability of a CEL expression & generate witness model")
+  static class CheckSatCommand extends SingleExpressionCommand {
+
+    @Override
+    public Integer call() {
+      return executeCommand(
+          (options, vars) ->
+              handleSingleResult(
+                  CelVerifierToolCore.checkSatisfiable(expression, vars, options),
+                  options.getOutputFormat()));
+    }
+  }
+
+  @Command(
+      name = "check-valid",
+      description = "Verify validity (isAlwaysTrue) of a CEL expression & generate counterexample")
+  static class CheckValidCommand extends SingleExpressionCommand {
+
+    @Override
+    public Integer call() {
+      return executeCommand(
+          (options, vars) ->
+              handleSingleResult(
+                  CelVerifierToolCore.checkValid(expression, vars, options),
+                  options.getOutputFormat()));
+    }
+  }
+
+  @Command(
+      name = "verify-equiv",
+      description = "Prove logical equivalence between two CEL expressions")
+  static class VerifyEquivCommand extends BaseVerificationCommand {
+
+    @Option(
+        names = {"--expr1"},
+        required = true,
+        description = "First CEL expression")
+    String expressionA = "";
+
+    @Option(
+        names = {"--expr2"},
+        required = true,
+        description = "Second CEL expression")
+    String expressionB = "";
+
+    @Override
+    public Integer call() {
+      return executeCommand(
+          (options, vars) ->
+              handleSingleResult(
+                  CelVerifierToolCore.verifyEquivalence(expressionA, expressionB, vars, options),
+                  options.getOutputFormat()));
+    }
+  }
+
+  @Command(
+      name = "verify-policy",
+      description = "Verify policy invariants defined in a YAML policy file")
+  static class VerifyPolicyCommand extends BaseVerificationCommand {
+
+    @Option(
+        names = {"--file", "-f"},
+        required = true,
+        description = "Path to policy YAML file")
+    String filePath = "";
+
+    @Override
+    public Integer call() {
+      return executeCommand(
+          "Policy verification error",
+          (options, vars) -> {
+            File file = new File(filePath);
+            if (!file.exists()) {
+              err().println("File not found: " + filePath);
+              return EXIT_CODE_ERROR;
+            }
+            String yamlContent =
+                new String(Files.readAllBytes(file.toPath()), StandardCharsets.UTF_8);
+
+            ImmutableMap<String, CelVerificationResult> results =
+                CelVerifierToolCore.verifyPolicyInvariants(yamlContent, vars, options);
+
+            if (options.getOutputFormat() == OutputFormat.JSON) {
+              out().println(FormatUtils.formatJsonPolicyResults(file.getName(), results));
+            } else {
+              out().println(FormatUtils.formatTextPolicyResults(file.getName(), results));
+            }
+
+            return getPolicyExitCode(results);
+          });
+    }
+
+    private static int getPolicyExitCode(ImmutableMap<String, CelVerificationResult> results) {
+      boolean anyViolated = false;
+      boolean anyInconclusive = false;
+      for (CelVerificationResult res : results.values()) {
+        if (res.status() == VerificationStatus.VIOLATED) {
+          anyViolated = true;
+        } else if (res.status() == VerificationStatus.INCONCLUSIVE) {
+          anyInconclusive = true;
+        }
+      }
+
+      if (anyViolated) {
+        return EXIT_CODE_VIOLATED;
+      } else if (anyInconclusive) {
+        return EXIT_CODE_INCONCLUSIVE;
+      }
+      return EXIT_CODE_VERIFIED;
+    }
+  }
+
+  public static void main(String[] args) {
+    int exitCode = new CommandLine(new CelVerifierTool()).execute(args);
+    System.exit(exitCode);
+  }
+}