Kani module stubs for development

[ajrudzitis]

Requested feature: Kani module stubs for development
Use case:

Kani is currently difficult to use in an IDE because the kani module is only injected when running cargo kani. This means that while writing harnesses in the IDE along with my code, the IDE does not recognize any statements like kani::any(). This adds friction to writing new test harnesses and I cannot use facilities in the IDE to identify issues before I run my harness.

If there could a module published that provided stubs for the Kani API, it would be useful for allowing the IDE to do basic type checks, etc.

[celinval]

Yes, this is definitely something that's been in our radar. I think this would also play nicely with things like #2035.

I think the main question is how to ensure compatibility between the crate version a user is importing and the one Kani is using. Especially if dependencies start exporting things like Arbitrary implementation.

[DianaNites]

I'm using cargo cfg dependencies to do this right now, and after a bit of trial and error it seems to be working. Kani helpfully has rather extensive documentation, which I can now see on hover and get autocomplete for.

---

The final working solution for code completion, documentation, error reporting, and highlighting under cfg(kani) code that I have arrived at is as follows.

It requires that rust-analyzer use nightly, because the kani crate uses nightly features, but I think thats fine, and it does not requiring using the same (pinned) nightly as kani does. (For example, I am currently on nightly-2025-05-04, but kani 0.62.0 is pinned to nightly-2025-04-24).

This solution also allows the crate to continue compiling on stable, if it otherwise does so. No nightly-only changes are required to Cargo.toml or otherwise.

---

The purpose of the Cargo.toml "dependency" is purely for IDE use, and the reason it uses a custom rust_analyzer cfg instead of kani is because otherwise the kani crate will exist twice when running cargo kani and conflict with itself.
This cfg is only for the IDE, and should not ever need to appear in your code, only normal cfg(kani) checks.

The specific name for this is unimportant and can be changed at any time, and it may be advisable to pick a unique cfg name for this case, something that dependencies are not likely to have used, to prevent spurious problems.

Cargo.toml is configured with a cfg / "platform specific" dependency.

[target.'cfg(rust_analyzer)'.dependencies.kani]
git = "https://github.com/model-checking/kani"
tag = "kani-0.62.0"

---

Rust-analyzer configured as follows, so that its analysis sees the kani dependency.

This also ignores the kani::proof macro, because it causes minor bugs with rust-analyzer highlighting, in my case i'm seeing inactive cfg blocks within proof functions no longer being dimmed properly when the macro is not ignored.

"rust-analyzer.cargo.extraEnv": {
    "RUSTFLAGS": "--cfg=rust_analyzer",
},
"rust-analyzer.procMacro.ignored": {
    "kani_macros": [
        "proof"
    ],
},

---

build.rs as follows, so that code is actually checked with the kani cfg set, thus errors are reported to RA and then to the IDE. The kani cfg is only set when our custom rust_analyzer cfg is also set, because otherwise it would interfere with normally building the crate, outside the IDE/Rust-Analyzer

Without this step you will get highlighting, completion, and hover documentation, but not error reporting / red squiggles for cfg(kani) blocks. They will also be dimmed.

--cfg=kani CANNOT be set in RUSTFLAGS

The reason why is that it will apply to all your dependencies, and if any of them happen to use kani themselves, their cfg(kani) blocks will be active, but they won't have the kani crate injected, and they likely dont depend on it in Cargo.toml the same way used here, resulting in spurious errors about the missing kani crate, and even if they do, it may?(i dont know if it will?) end up conflicting with your own git dependency, or result in incompatible type errors if you try to mix it with your usage.

Setting it in build.rs makes it apply only to your own crate.

This will have the side effect that you cant use Arbitrary implementations from dependencies if you wanted to without getting IDE errors. I don't believe there is any way around that while retaining error reporting for your own code, and I dont make use of this myself as of yet.

fn main() {
    println!("cargo::rerun-if-changed=build.rs");

    #[cfg(rust_analyzer)]
    println!("cargo::rustc-cfg=kani");
}

Note that the use of build.rs introduces a potential problem: --target. RUSTFLAGS stops applying to build scripts, so if you're developing for another platform, or set --target to your own for some other reason, you'll lose error reporting again. This is because of rust-lang/cargo#4423

There is a workaround, which also requires nightly: the cargo host-config unstable feature. In that case the following configuration for Rust-Analyzer should work, entirely through environment variables without requiring nightly-only persistent Cargo.toml changes.

The custom rust_analyzer cfg still needs to be set in RUSTFLAGS in this case, because otherwise it won't be picked up for the Cargo.toml dependency resolution of the kani crate.

"rust-analyzer.cargo.extraEnv": {
    "RUSTFLAGS": "--cfg=rust_analyzer",
    "CARGO_HOST_RUSTFLAGS": "--cfg=rust_analyzer",
    "CARGO_UNSTABLE_HOST_CONFIG": "true",
    "CARGO_UNSTABLE_TARGET_APPLIES_TO_HOST": "true",
    "CARGO_TARGET_APPLIES_TO_HOST": "false",
},