Add Kani smoke CI job (4.1.2)

.github/workflows/ci.yml

@@ -61,3 +61,33 @@ jobs:
           format: lcov
           access-token: ${{ env.CS_ACCESS_TOKEN }}
           installer-checksum: ${{ vars.CODESCENE_CLI_SHA256 }}
+
+  kani-smoke:
+    if: github.event_name == 'pull_request'
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    env:
+      CARGO_TERM_COLOR: always
+      RUSTUP_TOOLCHAIN: stable
+      CARGO_HOME: ${{ github.workspace }}/.kani-cargo
+      KANI_HOME: ${{ github.workspace }}/.kani-home
+    steps:
+      - uses: actions/checkout@9bb56186c3b09b4f86b1c65136769dd318469633  # v4.1.2
+        with:
+          persist-credentials: false
+      - name: Setup Rust
+        uses: leynos/shared-actions/.github/actions/setup-rust@6b13b519f99c5b461be8cc21ecf19c2ec5907b9c
+        with:
+          toolchain: stable
+      - name: Cache Kani tools
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830  # v4.3.0
+        with:
+          path: |
+            .kani-cargo
+            .kani-home
+          key: ${{ runner.os }}-kani-${{ hashFiles('tools/kani/VERSION', 'scripts/install-kani.sh') }}
+      - name: Install Kani
+        run: scripts/install-kani.sh
+      - name: Kani smoke
+        run: make kani

docs/developers-guide.md

@@ -76,8 +76,15 @@ Use the Make targets for day-to-day formal-verification checks:
 - `make formal-pr` aliases the pull-request formal-verification smoke path.
 
 Kani is intentionally not part of `make test`, `make lint`, `make check-fmt`,
-or `make all`. Formal verification remains opt-in until the dedicated Kani CI
-job is added by roadmap item `4.1.2`.
+or `make all`.
+
+Pull requests run a dedicated `kani-smoke` CI job alongside the ordinary
+`build-test` job. The job installs the pinned Kani version with
+`scripts/install-kani.sh` and runs only `make kani`; it does not run
+`make kani-full`, coverage, CodeScene upload, or the normal build matrix. Its
+cache is intentionally separate from ordinary Cargo build artefacts: the job
+uses a Kani-specific cache key derived from `tools/kani/VERSION` and caches the
+job-local Kani Cargo home plus Kani support-file home.
 
 ## Test suite map