[lalvesl]

Add a Nix flake: Kani releases, version selection and a development shell

First of all, thank you for building and maintaining Kani; it is a great and very helpful tool.

This PR solves the problems between Kani and Nix, for Linux and macOS users. With it, Kani works
with Nix out of the box: no ~/.kani, no rustup, no cargo kani setup, and no binary patching
when Kani runs. Users pick a Kani version, and Nix provides that exact release together with the
nightly toolchain it was built with:

pkgs.kaniReleases."0.67.0".kani   # Kani 0.67.0 + nightly-2025-11-21
pkgs.kaniReleases.latest.kani     # Kani 0.68.0 + nightly-2026-08-21

nix run github:model-checking/kani#kani -- file.rs   # the latest release
nix develop                                          # build Kani from source

Documentation:
nix/README.md.

Maintenance: automated, and the data is generated

The only hand-written part is the Nix code in nix/ and flake.nix. Everything that changes with
Kani's releases and dependencies is either read straight from files Kani already maintains, or
generated and updated by CI:

When this happens	What updates it	What a maintainer does
The nightly toolchain is bumped (rust-toolchain.toml)	Read directly from the file	Nothing
A Kani release is published	nix-versions-update.yml records it in nix/versions.json and opens a PR	Merge the PR
CBMC or Kissat is bumped (kani-dependencies)	Same workflow, at its next weekly run, records the new source hashes and opens a PR	Merge the PR
Anything else in Kani	Nothing to update	Nothing

• nix/versions.json is never edited by hand. It is generated by nix run .#update-versions,
  which reads each release from its kani-<version> tag and takes bundle hashes from the SHA-256
  digests GitHub publishes for release assets, so nothing is downloaded.
• If something is not recorded yet, Nix fails with a message naming the exact command to run,
  instead of building the wrong version.
• The pinned nixpkgs and rust-overlay in flake.lock keep working if never updated; refreshing
  them is optional.
• None of this touches Kani's Rust code, its setup path, or its existing CI. Users who do not use
  Nix are not affected.

The problem today

Kani's support for NixOS lives in src/os_hacks.rs. After cargo kani setup downloads the
bundle into ~/.kani, it patches the binaries with patchelf, and finds the C++ standard
library with nix-instantiate '<nixpkgs>'. This works on NixOS with channels, but:

• it needs NIX_PATH, which flake-only setups do not have;
• it only covers x86_64 Linux;
• the installation lives outside the Nix store, so it is neither reproducible nor pinned per
  project.

In #1298, it was suggested that "the most permanent solution" is proper Nix packaging. This PR
provides it, without changing the existing setup path.

How it works

• Official binaries. kaniReleases.<version>.kani is the official release bundle from
  GitHub releases, the same file cargo kani setup downloads. It is installed in the Nix store,
  with its toolchain link pointing at the matching nightly from rust-overlay. Kani is not
  rebuilt.
• Safety check at build time. The build fails if that toolchain's rustc --version differs
  from the rustc-version recorded in the bundle.
• Platform handling. On Linux, the bundled binaries (Kani, CBMC, Kissat) are patched with
  autoPatchelfHook, which rewrites only their dynamic linker and library search path. On macOS
  they are used unchanged, because they already find the toolchain through
  @loader_path/../toolchain/lib.
• Development shell without rustup. kani-compiler/build.rs reads RUSTUP_HOME and
  RUSTUP_TOOLCHAIN, and kani-driver runs cargo +<toolchain> from a development checkout. A
  small shim provides both, so cargo build-dev works in nix develop without rustup.
• Releases read from tags. Release data comes from the tags, not the working tree. After a
  release, main keeps the released version in Cargo.toml while its toolchain moves on. For
  example, main says 0.68.0 on nightly-2026-10-23, but the 0.68.0 release was built with
  nightly-2026-08-21.

Files

Path	What
flake.nix, flake.lock	The flake: overlays, packages, devShells
nix/overlay.nix	kaniPackages (this checkout) and kaniReleases.<version>
nix/pkgs/kani-bin.nix	Kani from its release bundle
nix/pkgs/rustup-shim.nix, nix/pkgs/dev-shell.nix	Development shell
nix/pkgs/update-versions.{sh,nix}, nix/versions.json	Release data (generated) and its generator
.github/workflows/nix-versions-update.yml	Keeps nix/versions.json up to date
scripts/ci/copyright-exclude	Excludes the generated flake.lock, like Cargo.lock

Testing

Automated, in CI:

• kani-nix-example-PR5098 is a small crate with proofs
  adapted from the tutorial. It has one shell per Kani version (nix develop .#kani-latest,
  nix develop .#kani-0_67) and runs cargo kani in each, on x86_64 Linux, aarch64 Linux and
  aarch64 macOS. All 6 jobs pass:
  run.
• On my fork, this branch passes Kani CI, Format Check (including the copyright check) and Cargo
  Deny.

Why Nix, briefly

For readers less familiar with Nix: it is a package manager that installs every package into its
own directory, identified by a hash of everything it was built from. For Kani, that means:

• Reproducible. A project's flake.lock pins the exact Kani release, nightly toolchain and
  CBMC. Everyone on the project, and its CI, gets the same files, checked against those hashes.
• One command to set up. nix develop gives a shell with Kani ready to use. There is no
  installation step and no cargo kani setup.
• Versions side by side. Two projects can use different Kani versions on the same machine
  without conflicts, because nothing is installed globally (~/.kani, rustup toolchains).
• Same on Linux and macOS. The same flake works on both, with no per-OS setup steps.
• Nothing left behind. Leaving the shell leaves the system unchanged.

Manual, on NixOS (x86_64):

• nix flake check passes.
• In nix develop, cargo build-dev succeeds, and ./scripts/kani verifies a sample harness.
• Kani 0.67.0 and 0.68.0 build from their bundles and verify the example crate.
• CBMC 6.8.0 (bundles CaDiCaL 2.0.0) and 6.11.0 (bundles CaDiCaL 3.0.0) build from source.
• update-versions is idempotent: rerunning it for a recorded release leaves versions.json
  byte-for-byte unchanged.

Not tested: x86_64 macOS. GitHub no longer offers Intel macOS runners, and I have no access to
such a machine.

Alternative layout

If you would prefer the release catalog (nix/versions.json and its workflow) outside this
repository, it can move into a separate overlay repository, and this repository would keep only
the development shell. I am happy to split it that way.

Related: #1179, #1298, #2207, #4413

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.