test infra: Kani for unsafe-heavy crates

[JonasKruckenberg]

Problem

k23 has a lot of unsafe. Particularly in sys/kernel/src/wasm/vm/ (vmcontext.rs, instance.rs) this is part of the sandbox boundary code. Nothing machine-checks these invariants today.

Goal

Kani is a bounded model checker for Rust. That we should add as a first-class test type.

Lets begin with a small initial set crates (or just one) that is easily tested. E.g.:

• lib/spin::Mutex Only one MutexGuard exists at a time (2–3 threads)

Plan

Step 1 — build/kani.bzl

Just like build/loom.bzl or build/fuzz.bzl. Declares rust_kani_proof(), which compiles with --cfg=kani and runs kani-driver via a wrapper script. Kani only runs on the host afaik. Don't forget to add the labels = ["kani"] label so we can filter for these tests later.

Step 2 — justfile

@kani targets="" *buck2_args:
    {{ _buck2 }} test {{_uquery(_q_kani_proofs(_targets_query(targets)))}} ...

Step 3 — curated fast preflight subset

Kani proofs take a while. Only harnesses tagged ["kani", "preflight"] run in just preflight (target: <30s each). Everything else runs nightly. TODO we should verify this is actually needed

Step 4 — Nightly CI (.github/workflows/kani.yml)

Full just kani runs nightly.

References

• [Kani](https://github.com/model-checking/kani) · [Firecracker case study](https://aws.amazon.com/blogs/opensource/how-open-source-projects-are-using-kani-to-write-better-software-in-rust/) · [Merlin OS case study](https://paolozaino.wordpress.com/2025/08/08/merlin-os-building-trust-in-risc-os-merlin-with-formal-verification-methods/) · [verify-rust-std](https://github.com/model-checking/verify-rust-std)