Experiment with Bazel as a build system.

.bazelversion

@@ -0,0 +1 @@
+9.1.1

.cargo/config.toml

@@ -6,3 +6,7 @@
 # the header lives in /usr/include/z3/ rather than /usr/include/. The extra -I
 # is harmless on systems where the path doesn't exist.
 BINDGEN_EXTRA_CLANG_ARGS = "-I/usr/include/z3"
+
+# Location of the shared protobuf tree, consumed by openshell-core's build.rs.
+# Bazel builds inject this via build_script_env instead.
+OPENSHELL_PROTO_DIR = { value = "proto", relative = true }

.github/workflows/ci.yml

@@ -0,0 +1,28 @@
+name: CI
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  bazel:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: bazel-contrib/setup-bazel@c5acdfb288317d0b5c0bbd7a396a3dc868bb0f86 # 0.19.0
+        with:
+          bazelisk-cache: true
+          disk-cache: ${{ github.workflow }}
+          repository-cache: true
+
+      - name: Test (host)
+        run: bazel test //...
+
+      - name: Build (linux amd64 musl)
+        run: bazel build //... --platforms=//:linux_amd64_musl
+
+      - name: Build (linux arm64 musl)
+        run: bazel build //... --platforms=//:linux_arm64_musl

.gitignore

@@ -226,6 +226,9 @@ rfc.md
 # Markdown/mermaid lint tooling deps
 scripts/lint-mermaid/node_modules/
 
+# Bazel convenience symlinks
+bazel-*
+
 # Nix
 /result
 /result-*

BUILD.bazel

@@ -0,0 +1,31 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+# Short local names for the static release platforms; toolchain selection
+# happens via the platforms' @zig_sdk//libc:musl constraint.
+platform(
+    name = "linux_amd64_musl",
+    parents = ["@zig_sdk//libc_aware/platform:linux_amd64_musl"],
+)
+
+platform(
+    name = "linux_arm64_musl",
+    parents = ["@zig_sdk//libc_aware/platform:linux_arm64_musl"],
+)
+
+# Experimental: cross-compiling library crates to macOS. zig provides the
+# darwin libc headers and libSystem stubs; targets needing Apple framework
+# link stubs (Security, CoreFoundation) cannot link without an Apple SDK.
+platform(
+    name = "darwin_arm64",
+    parents = ["@zig_sdk//platform:darwin_arm64"],
+)
+
+# The Bazel-built z3 install tree (include/ + lib/) as one directory
+# artifact, consumed by the z3-sys crate annotation in bazel/rust.MODULE.bazel.
+filegroup(
+    name = "z3_install",
+    srcs = ["@z3//:z3_static"],
+    output_group = "gen_dir",
+    visibility = ["//visibility:public"],
+)

MODULE.bazel

@@ -0,0 +1,17 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+module(
+    name = "openshell",
+    version = "0.0.0",
+)
+
+bazel_dep(name = "platforms", version = "1.1.0")
+bazel_dep(name = "rules_cc", version = "0.2.17")
+
+# The rest of the build config lives in bazel/, split by concern.
+include("//bazel:rust.MODULE.bazel")
+
+include("//bazel:cc_toolchains.MODULE.bazel")
+
+include("//bazel:z3.MODULE.bazel")

bazel/BUILD.bazel

@@ -0,0 +1,5 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+# Package marker so the MODULE.bazel include() segments in this directory
+# resolve as labels. Build targets live in the sibling packages.

bazel/cc_toolchains.MODULE.bazel

@@ -0,0 +1,40 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+# C/C++ toolchain providers: zig (cross-compilation), protoc, and libclang.
+
+bazel_dep(name = "hermetic_cc_toolchain", version = "4.1.0")
+
+hermetic_toolchain = use_extension("@hermetic_cc_toolchain//toolchain:ext.bzl", "toolchains")
+use_repo(hermetic_toolchain, "zig_sdk")
+
+# Only match platforms carrying @zig_sdk//libc:musl — dormant for dev builds,
+# which keep the autodetected host toolchain.
+register_toolchains(
+    "@zig_sdk//libc_aware/toolchain:linux_amd64_musl",
+    "@zig_sdk//libc_aware/toolchain:linux_arm64_musl",
+    "@zig_sdk//toolchain:darwin_arm64",
+)
+
+# Hermetic protoc for openshell-core's build script, injected via $PROTOC
+# instead of the autotools build that protobuf-src does under cargo. Built
+# from source in the exec configuration (one-time cost, then cached).
+bazel_dep(name = "protobuf", version = "33.4")
+
+# Prebuilt LLVM distribution as the source of libclang for z3-sys's bindgen
+# run (the same route rules_rust's bindgen_toolchain example takes; building
+# LLVM from source needs an older C++ toolchain than ours). Deliberately not
+# registered as a cc toolchain — zig and the host autodetect own that space.
+bazel_dep(name = "toolchains_llvm", version = "1.8.0")
+
+llvm = use_extension("@toolchains_llvm//toolchain/extensions:llvm.bzl", "llvm")
+llvm.toolchain(
+    name = "llvm_toolchain",
+    llvm_version = "20.1.4",
+)
+use_repo(llvm, "llvm_toolchain_llvm")
+
+# The prebuilt libclang.so dynamically links libz.so.1 and expects it from
+# the host, which NixOS does not serve; a Bazel-built one is bundled next to
+# it instead (see //bazel/clang:libclang_bundle).
+bazel_dep(name = "zlib", version = "1.3.1.bcr.5")

bazel/clang/BUILD.bazel

@@ -0,0 +1,44 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+# libclang plumbing for z3-sys's bindgen run: the prebuilt LLVM libclang, the
+# libz.so.1 it expects from the host (which NixOS does not serve), and clang's
+# builtin headers. Kept together because the prebuilt binary's runtime
+# expectations are the whole problem this package exists to solve.
+
+load("@rules_cc//cc:cc_shared_library.bzl", "cc_shared_library")
+
+# A libz.so.1 whose exports carry the ZLIB_1.2.0 symbol version that the
+# prebuilt libclang references; the BCR zlib's cc_library omits it (see
+# zlib.map).
+cc_shared_library(
+    name = "z_shared",
+    additional_linker_inputs = ["zlib.map"],
+    user_link_flags = ["-Wl,--version-script=$(location zlib.map)"],
+    deps = ["@zlib//:z"],
+)
+
+# libclang next to that libz.so.1. libclang's RUNPATH is $ORIGIN/../lib, so a
+# sibling libz in the same lib/ dir resolves without patching the binary.
+genrule(
+    name = "libclang_bundle",
+    srcs = [
+        ":z_shared",
+        "@llvm_toolchain_llvm//:libclang",
+    ],
+    outs = [
+        "libclang/lib/libclang.so",
+        "libclang/lib/libz.so.1",
+    ],
+    cmd = "cp $(execpath @llvm_toolchain_llvm//:libclang) $(RULEDIR)/libclang/lib/libclang.so && " +
+          "cp $(execpath :z_shared) $(RULEDIR)/libclang/lib/libz.so.1",
+    visibility = ["//visibility:public"],
+)
+
+# Clang's builtin headers (stdbool.h etc.), which libclang would normally find
+# relative to its binary but cannot in the stripped bundle above.
+alias(
+    name = "clang_builtin_include",
+    actual = "@llvm_toolchain_llvm//:lib/clang/20/include",
+    visibility = ["//visibility:public"],
+)

bazel/clang/zlib.map

@@ -0,0 +1,7 @@
+/* The prebuilt libclang references zlib symbols tagged ZLIB_1.2.0, but the
+ * BCR zlib's cc_library build exports them untagged. Re-apply the symbol
+ * version upstream zlib's own Makefile would (see :libclang_bundle). */
+ZLIB_1.2.0 {
+    global:
+        *;
+};

bazel/rust.MODULE.bazel

@@ -0,0 +1,95 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+# Rust toolchains and the crate_universe dependency graph.
+
+bazel_dep(name = "rules_rust", version = "0.71.3")
+
+rust = use_extension("@rules_rust//rust:extensions.bzl", "rust")
+
+rust.toolchain(
+    edition = "2024",
+    versions = ["1.95.0"],
+)
+
+# Musl toolchains for static release builds. Their @zig_sdk//libc:musl
+# constraint keeps them dormant on the (constraint-less) host platform, so
+# dev builds are unaffected.
+rust.repository_set(
+    name = "rust_linux_amd64_musl",
+    exec_triple = "x86_64-unknown-linux-gnu",
+    target_triple = "x86_64-unknown-linux-musl",
+    versions = ["1.95.0"],
+    extra_rustc_flags = ["-Clink-self-contained=no"],
+    target_compatible_with = [
+        "@platforms//os:linux",
+        "@platforms//cpu:x86_64",
+        "@zig_sdk//libc:musl",
+    ],
+)
+
+rust.repository_set(
+    name = "rust_linux_arm64_musl",
+    exec_triple = "x86_64-unknown-linux-gnu",
+    target_triple = "aarch64-unknown-linux-musl",
+    versions = ["1.95.0"],
+    extra_rustc_flags = ["-Clink-self-contained=no"],
+    target_compatible_with = [
+        "@platforms//os:linux",
+        "@platforms//cpu:aarch64",
+        "@zig_sdk//libc:musl",
+    ],
+)
+
+# Experimental macOS cross-compilation (library crates only; linking needs
+# Apple framework stubs that zig does not ship).
+rust.repository_set(
+    name = "rust_darwin_arm64",
+    exec_triple = "x86_64-unknown-linux-gnu",
+    target_triple = "aarch64-apple-darwin",
+    versions = ["1.95.0"],
+    target_compatible_with = [
+        "@platforms//os:macos",
+        "@platforms//cpu:aarch64",
+    ],
+)
+
+use_repo(rust, "rust_toolchains")
+
+# The musl hub entries must be registered before //:all — the gnu entries in
+# the hub also match musl platforms (they declare no libc constraint), and
+# Bazel picks the first compatible registration.
+register_toolchains(
+    "@rust_toolchains//:rust_linux_amd64_musl__x86_64-unknown-linux-musl__stable",
+    "@rust_toolchains//:rust_linux_arm64_musl__aarch64-unknown-linux-musl__stable",
+)
+
+register_toolchains("@rust_toolchains//:all")
+
+crate = use_extension("@rules_rust//crate_universe:extensions.bzl", "crate")
+crate.from_cargo(
+    name = "crates",
+    cargo_lockfile = "//:Cargo.lock",
+    manifests = [
+        "//:Cargo.toml",
+    ],
+)
+
+# Under cargo, z3-sys links the system libz3; here it gets the Bazel-built
+# one: the header for its bindgen run and the lib directory for linking.
+crate.annotation(
+    crate = "z3-sys",
+    build_script_data = [
+        "@@//:z3_install",
+        "@@//bazel/clang:clang_builtin_include",
+        "@@//bazel/clang:libclang/lib/libclang.so",
+        "@@//bazel/clang:libclang/lib/libz.so.1",
+    ],
+    build_script_env = {
+        "BINDGEN_EXTRA_CLANG_ARGS": "-isystem $(execpath @@//bazel/clang:clang_builtin_include)",
+        "LIBCLANG_PATH": "$(execpath @@//bazel/clang:libclang/lib/libclang.so)",
+        "Z3_LIBRARY_PATH_OVERRIDE": "$(execpath @@//:z3_install)/lib",
+        "Z3_SYS_Z3_HEADER": "$(execpath @@//:z3_install)/include/z3.h",
+    },
+)
+use_repo(crate, "crates")

bazel/z3.MODULE.bazel

@@ -0,0 +1,20 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+# Bazel-built libz3 for openshell-prover, injected into z3-sys instead of the
+# system library that plain cargo links. The BCR module is a year stale, so
+# override with the upstream release, which carries its own MODULE.bazel.
+bazel_dep(name = "z3", version = "4.16.0")
+
+archive_override(
+    module_name = "z3",
+    # z3's BUILD.bazel collects install outputs from lib/, but CMake's
+    # GNUInstallDirs host-sniffs the layout and picks lib64/ on non-Debian
+    # Linux. Pin the libdir right after each generator declaration.
+    patch_cmds = [
+        """sed -i '/-G Ninja/a\\        "-D CMAKE_INSTALL_LIBDIR=lib",' BUILD.bazel""",
+    ],
+    integrity = "sha256-xow+XkgQsWEmuMtMR+7oXBrD4kqBkUyONxtA3p3TOsc=",
+    strip_prefix = "z3-z3-4.16.0",
+    urls = ["https://github.com/Z3Prover/z3/archive/refs/tags/z3-4.16.0.tar.gz"],
+)

crates/openshell-bootstrap/BUILD.bazel

@@ -0,0 +1,22 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+load("@crates//:defs.bzl", "all_crate_deps")
+load("@rules_rust//rust:defs.bzl", "rust_library", "rust_test")
+
+rust_library(
+    name = "openshell_bootstrap",
+    srcs = glob(["src/**/*.rs"]),
+    edition = "2024",
+    visibility = ["//visibility:public"],
+    deps = all_crate_deps(normal = True) + [
+        "//crates/openshell-core:openshell_core",
+    ],
+    proc_macro_deps = all_crate_deps(proc_macro = True),
+)
+
+rust_test(
+    name = "openshell_bootstrap_test",
+    crate = ":openshell_bootstrap",
+    deps = all_crate_deps(normal_dev = True),
+)

crates/openshell-cli/BUILD.bazel

@@ -0,0 +1,43 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+load("@crates//:defs.bzl", "all_crate_deps")
+load("@rules_rust//rust:defs.bzl", "rust_binary", "rust_library", "rust_test")
+
+WORKSPACE_DEPS = [
+    "//crates/openshell-bootstrap:openshell_bootstrap",
+    "//crates/openshell-core:openshell_core",
+    "//crates/openshell-policy:openshell_policy",
+    "//crates/openshell-providers:openshell_providers",
+    "//crates/openshell-prover:openshell_prover",
+    "//crates/openshell-tui:openshell_tui",
+]
+
+rust_library(
+    name = "openshell_cli",
+    srcs = glob(
+        ["src/**/*.rs"],
+        exclude = ["src/main.rs"],
+    ),
+    edition = "2024",
+    visibility = ["//visibility:public"],
+    deps = all_crate_deps(normal = True) + WORKSPACE_DEPS,
+    proc_macro_deps = all_crate_deps(proc_macro = True),
+)
+
+rust_binary(
+    name = "openshell",
+    srcs = ["src/main.rs"],
+    edition = "2024",
+    visibility = ["//visibility:public"],
+    deps = all_crate_deps(normal = True) + WORKSPACE_DEPS + [
+        ":openshell_cli",
+    ],
+    proc_macro_deps = all_crate_deps(proc_macro = True),
+)
+
+rust_test(
+    name = "openshell_cli_test",
+    crate = ":openshell_cli",
+    deps = all_crate_deps(normal_dev = True),
+)