devenv: Add Kani formal verification tool

Kani is a bounded model checker for Rust that can verify safety properties
and absence of undefined behavior. It requires rustup because it bundles a
specific nightly toolchain version.

Key changes:
- Add rustup symlink at $CARGO_HOME/bin/rustup (required for rustup's
  self-update check which looks for itself there)
- Add new 'kani' build stage that compiles kani-verifier and runs setup
- Set KANI_HOME=/usr/local/kani for system-wide installation
- Copy kani bundle (compiler, libraries, CBMC) to final image

The kani version is renovate-managed via the kaniversion ARG.

Assisted-by: OpenCode (Claude Sonnet 4)
Signed-off-by: Colin Walters <walters@verbum.org>

Author: cgwalters

devenv/Containerfile.c10s

@@ -90,8 +90,34 @@ export CARGO_HOME=/usr/local/cargo
 curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile default
 # Move binaries to /usr/local/bin (system-managed, root-owned)
 mv /usr/local/cargo/bin/* /usr/local/bin/
-# Nothing really left here
-rm -vrf /usr/local/cargo/bin
+# Recreate bin directory with symlink to rustup - rustup's self-update check
+# looks for itself at $CARGO_HOME/bin/rustup
+mkdir -p /usr/local/cargo/bin
+ln -sf /usr/local/bin/rustup /usr/local/cargo/bin/rustup
+EORUN
+
+# Kani formal verification tool - requires rustup for toolchain management
+FROM rust as kani
+# renovate: datasource=crate depName=kani-verifier
+ARG kaniversion=0.67.0
+RUN <<EORUN
+set -xeuo pipefail
+# Install build dependencies needed to compile kani-verifier
+dnf install -y gcc
+export RUSTUP_HOME=/usr/local/rustup
+export CARGO_HOME=/usr/local/cargo
+export PATH="/usr/local/bin:$PATH"
+# Install Kani to a system-wide location so all users can access it
+export KANI_HOME=/usr/local/kani
+
+# Install kani-verifier
+/bin/time -f '%E %C' cargo install --locked kani-verifier --version $kaniversion
+
+# Run kani setup - downloads bundle and installs required nightly toolchain
+/bin/time -f '%E %C' /usr/local/cargo/bin/cargo-kani setup
+
+# Move kani binaries to /usr/local/bin, keep rustup symlink
+mv /usr/local/cargo/bin/cargo-kani /usr/local/cargo/bin/kani /usr/local/bin/
 EORUN
 
 # This builds the image.
@@ -110,10 +136,14 @@ RUN grep -vEe '^#' npm.txt | /bin/time -f '%E %C' xargs npm i -g
 
 # Copy in the binaries from our tools container image
 COPY --from=tools /usr/local/bin/* /usr/local/bin/
-COPY --from=rust /usr/local/bin/* /usr/local/bin/
-COPY --from=rust /usr/local/rustup /usr/local/rustup
+COPY --from=kani /usr/local/bin/* /usr/local/bin/
+COPY --from=kani /usr/local/rustup /usr/local/rustup
+# Kani bundle (compiler, libraries, CBMC) installed via KANI_HOME during setup
+COPY --from=kani /usr/local/kani /usr/local/kani
 # Point rustup at the system-wide installation, but let CARGO_HOME default to ~/.cargo
 ENV RUSTUP_HOME=/usr/local/rustup
+# Point Kani at the system-wide installation
+ENV KANI_HOME=/usr/local/kani
 # Setup for codespaces
 COPY devenv-init.sh /usr/local/bin/
 

devenv/Containerfile.debian

@@ -88,8 +88,34 @@ export CARGO_HOME=/usr/local/cargo
 curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable --profile default
 # Move binaries to /usr/local/bin (system-managed, root-owned)
 mv /usr/local/cargo/bin/* /usr/local/bin/
-# Nothing really left here
-rm -vrf /usr/local/cargo/bin
+# Recreate bin directory with symlink to rustup - rustup's self-update check
+# looks for itself at $CARGO_HOME/bin/rustup
+mkdir -p /usr/local/cargo/bin
+ln -sf /usr/local/bin/rustup /usr/local/cargo/bin/rustup
+EORUN
+
+# Kani formal verification tool - requires rustup for toolchain management
+FROM rust as kani
+# renovate: datasource=crate depName=kani-verifier
+ARG kaniversion=0.67.0
+RUN <<EORUN
+set -xeuo pipefail
+# Install build dependencies needed to compile kani-verifier
+apt-get update && apt-get install -y --no-install-recommends build-essential
+export RUSTUP_HOME=/usr/local/rustup
+export CARGO_HOME=/usr/local/cargo
+export PATH="/usr/local/bin:$PATH"
+# Install Kani to a system-wide location so all users can access it
+export KANI_HOME=/usr/local/kani
+
+# Install kani-verifier
+/bin/time -f '%E %C' cargo install --locked kani-verifier --version $kaniversion
+
+# Run kani setup - downloads bundle and installs required nightly toolchain
+/bin/time -f '%E %C' /usr/local/cargo/bin/cargo-kani setup
+
+# Move kani binaries to /usr/local/bin, keep rustup symlink
+mv /usr/local/cargo/bin/cargo-kani /usr/local/cargo/bin/kani /usr/local/bin/
 EORUN
 
 # This builds the image.
@@ -108,10 +134,14 @@ RUN grep -vEe '^#' npm.txt | /bin/time -f '%E %C' xargs npm i -g
 
 # Copy in the binaries from our tools container image
 COPY --from=tools /usr/local/bin/* /usr/local/bin/
-COPY --from=rust /usr/local/bin/* /usr/local/bin/
-COPY --from=rust /usr/local/rustup /usr/local/rustup
+COPY --from=kani /usr/local/bin/* /usr/local/bin/
+COPY --from=kani /usr/local/rustup /usr/local/rustup
+# Kani bundle (compiler, libraries, CBMC) installed via KANI_HOME during setup
+COPY --from=kani /usr/local/kani /usr/local/kani
 # Point rustup at the system-wide installation, but let CARGO_HOME default to ~/.cargo
 ENV RUSTUP_HOME=/usr/local/rustup
+# Point Kani at the system-wide installation
+ENV KANI_HOME=/usr/local/kani
 # Setup for codespaces
 COPY devenv-init.sh /usr/local/bin/