feat(cuda-device): prove witness arithmetic with Kani

.github/workflows/ci.yml

@@ -35,7 +35,7 @@ concurrency:
   cancel-in-progress: ${{ github.ref_name != 'main' }}
 
 # Every other workflow in the repo pins this rather than inheriting whatever the
-# repository default happens to be. This one is a pure caller today, so the four
+# repository default happens to be. This one is a pure caller today, so the five
 # called workflows' own `contents: read` already bounds the token and this
 # changes nothing. It matters for the next job added here directly: a `uses:`
 # job carries the callee's permissions, an inline `steps:` job would carry the
@@ -55,3 +55,6 @@ jobs:
 
   cargo-deny:
     uses: ./.github/workflows/cargo-deny.yml
+
+  kani:
+    uses: ./.github/workflows/kani.yml

.github/workflows/kani.yml

@@ -0,0 +1,63 @@
+# SPDX-FileCopyrightText: Copyright (c) 2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
+# SPDX-License-Identifier: Apache-2.0
+---
+name: kani
+
+# Runs as a job of the top-level CI workflow (.github/workflows/ci.yml),
+# which is the single push/pull_request entry point. Concurrency is governed
+# by CI's own group, so this workflow declares none of its own.
+on:
+  workflow_call:
+
+permissions:
+  contents: read
+
+env:
+  KANI_VERSION: 0.68.0
+  # `cargo kani` compiles with the nightly `cargo kani setup` installs and
+  # ignores both rust-toolchain.toml pins, but the rustup `cargo` proxy would
+  # still install the pinned toolchain (cuda-oxide's nightly with rustc-dev)
+  # just to dispatch the subcommand. The runner's stable is enough for that.
+  RUSTUP_TOOLCHAIN: stable
+
+jobs:
+  kani:
+    name: kani ${{ matrix.gate }}
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - gate: prove
+            script: scripts/kani.sh
+          - gate: mutants
+            script: scripts/kani-mutants.sh
+    steps:
+      - name: Clone repository
+        uses: actions/checkout@v4
+
+      # Only the `cargo install` binaries are cached. `cargo kani setup`
+      # links ~/.kani to a nightly under ~/.rustup, so caching ~/.kani alone
+      # would restore a dangling toolchain link; setup reruns every time.
+      - name: Cache cargo-kani
+        id: cache-kani
+        uses: actions/cache@v4
+        with:
+          path: |
+            ~/.cargo/bin/cargo-kani
+            ~/.cargo/bin/kani
+          key: kani-verifier-${{ env.KANI_VERSION }}-${{ runner.os }}
+
+      - name: Install Kani
+        run: |
+          set -euo pipefail
+          if [ "${{ steps.cache-kani.outputs.cache-hit }}" != "true" ]; then
+            cargo install --locked kani-verifier --version "${KANI_VERSION}"
+          fi
+          cargo kani setup
+          cargo kani --version
+
+      - name: Run ${{ matrix.script }}
+        working-directory: cuda-oxide
+        run: bash ${{ matrix.script }}

cuda-oxide/Justfile

@@ -89,6 +89,14 @@ test-cuda:
     cargo test --all-targets \
         -p cuda-oxide-codegen -p cuda-macros -p cuda-host
 
+# Prove the cuda-device witness arithmetic with Kani (needs cargo-kani 0.68.0)
+kani *args:
+    bash scripts/kani.sh {{args}}
+
+# Require every kani-mutants/ fault to fail its Kani harnesses (needs cargo-kani 0.68.0)
+kani-mutants *args:
+    bash scripts/kani-mutants.sh {{args}}
+
 # Mirror unit-tests.yml's third job, `generated-intrinsics`: the three gates a
 # change under crates/cuda-intrinsics-gen has to pass. Nothing else here ran
 # them, so a catalog edit could clear `just check` and still fail CI -- and the
@@ -130,7 +138,7 @@ doc-check:
 # per example workspace), examples-compile (needs the CUDA codegen backend),
 # and CodeQL. The book gate has a local mirror too, but `just book` stays out
 # of `check` as the one gate needing a Python virtualenv.
-# Run CI's gates minus examples-compile, book, CodeQL
+# Run CI's gates minus examples-compile, book, kani, CodeQL
 check: fmt-check clippy test test-cuda check-guards check-intrinsics doc-check
 
 # Clean project-local Cargo outputs and known cuda-oxide artifacts

cuda-oxide/crates/cuda-device/Cargo.toml

@@ -22,4 +22,7 @@ trybuild = "1"
 [lints.rust]
 # `cargo oxide` owns this cfg and enables it only for full device debug. Declare
 # it here so ordinary workspace builds validate the conditional annotation too.
-unexpected_cfgs = { level = "warn", check-cfg = ["cfg(cuda_oxide_internal_outline_disjoint_get_mut_v1)"] }
+unexpected_cfgs = { level = "warn", check-cfg = [
+    "cfg(cuda_oxide_internal_outline_disjoint_get_mut_v1)",
+    "cfg(kani)",
+] }