[calef]

This PR adds an unstable --target <TRIPLE> option, so Kani can verify a crate for a target other than the host, and adds riscv64gc-unknown-linux-gnu as a target Kani has a machine model for.

Towards #2402. It covers the part of that issue that needs no new machine-model work: 64-bit little-endian targets. The 16-bit and big-endian cases asked for there are left for later (see "Not in this PR").

Why

CBMC does not care which machine it runs on; the machine model is data Kani writes into the goto program. What stops Kani verifying for another target today is that four places are keyed to env!("TARGET"): the target passed to cargo, the sysroot build-kani builds, check_target's allowlist, and new_machine_model. Our use is a kernel with an arch/riscv64 tree whose code only compiles for riscv64 (cfg(target_arch), core::arch::riscv64), which we want to prove from x86_64 and Apple Silicon machines, including GitHub-hosted runners. CBMC 6.11's set_arch_spec_riscv64 already exists, so CBMC needs no change.

What changes

• kani-compiler: a riscv64 machine model (RISC-V psABI LP64D: unsigned char, signed 32-bit wchar_t, 128-bit long double, matching CBMC's set_arch_spec_riscv64), riscv64-unknown-linux-gnu in check_target, and the riscv64gc target features in target_config. Without d there, rustc warns on every crate that the LP64D ABI needs it, and says the warning will become an error.
• kani-driver: --target <TRIPLE>, gated on -Z unstable-options, for both kani and cargo kani. It replaces env!("TARGET") in the cargo invocation, cargo metadata --filter-platform, the coverage paths and the single-file rustc call. When it is not given, nothing changes: the host triple is used exactly as before, and single-file runs do not pass --target to rustc at all. --concrete-playback with a non-host --target is rejected (the test runs on the host), and so is verify-std --target (its no_core library is host-only).
• Libraries for more than one target: cargo build-dev --lib-target <TRIPLE> (repeatable) also builds the verification libraries for that triple into target/kani/targets/<TRIPLE>/lib/, which is a complete sysroot of its own. The host keeps lib/ exactly as it is, so release bundles and cargo kani setup are unaffected. The driver looks for a non-host target's libraries there, and if they are missing it says which command builds them. The rustup target does not need to be installed, since -Z build-std builds from rust-src.
• Docs: a page under Experimental features.

Testing

• New tests/script-based-pre/target_riscv64. It runs kani on a single file and cargo kani on a crate, both for riscv64. The harnesses sit behind #[cfg(target_arch = "riscv64")], so the test also shows that the host run finds none. They check target facts that differ from an x86_64 host (c_char is unsigned, target_feature = "d"), and there is one failing overflow check, so CBMC has to find something. The crate's harness stubs a function that uses rdcycle inline assembly, which does not compile for any other target. The test also covers the error when -Z unstable-options is missing, and the --concrete-playback and verify-std rejections. The missing-library error has no transcript-stable test: every target check_target accepts has its libraries built somewhere in the CI matrix (riscv64's by kani-regression.sh, below), so the error cannot be triggered there.
• scripts/kani-regression.sh now builds with --lib-target riscv64gc-unknown-linux-gnu so this test runs in CI. That adds one library build to each of the five regression matrix jobs; on an Apple Silicon Mac it took about two minutes, under heavy load from other work. I can move it to a single separate job if you would rather keep it off the main regression path. None of the regression workflows have run on this PR yet; they are waiting for approval to run for a first-time contributor.
• Local runs on aarch64 macOS with CBMC 6.11.0: cargo test -p kani-driver -p kani_metadata -p build-kani, ./scripts/kani-fmt.sh --check, and the compiletest suites ui (152 passed), cargo-ui (30), cargo-kani (71), expected (478 passed, 16 ignored) and cargo-coverage (2). On 2026-10-03, rebased on main at 1640445da, script-based-pre passed (91, 1 ignored), ui passed (153) and cargo-ui passed (30). The verify_std_cmd failure I mentioned earlier did not recur. I have not run the coverage suite. I did not run the full kani suite or firecracker locally.
• Out of tree, a patch equivalent to this one against 0.67.0 compiled a whole no_std kernel crate for riscv64 and verified its harnesses, stubs included.

Something I noticed and did not change

When goto-cc links goto binaries, the first input's __CPROVER_architecture_* symbols win, and link_goto_binary passes kani_lib.c as C source, which goto-cc compiles with the host's configuration. So the linked .out carries the host's architecture (arm64 and char_is_unsigned = 0 on Apple Silicon) rather than the model Kani wrote. Precompiling kani_lib.c and linking it after the Rust inputs would fix it; I'd propose that as a follow-up.

Not in this PR

• 32-bit targets (goto-cc -m32, plus the 64-bit assumptions @celinval mentioned in How to verify a target different to the host environment? #2086), 16-bit usize, and big-endian targets, all of which Command-line flag to change model target or environment  #2402 asks for.
• Non-host libraries in release bundles and in cargo kani setup.
• A dedicated -Z feature name. This uses -Z unstable-options, like other experimental options. If you would prefer a named feature, or an RFC first, I'll do that.

Disclosure

This change was written by an AI coding agent (Claude Code) working under my direction, for nife, a capability microkernel that uses Kani for its kernel proofs. I'm responsible for it and will follow up on review.

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

[tautschnig]

Thank you for your contribution! A couple of comments inline.

[calef]

I've pushed a small follow-up (450cbc2): --lib-target now conflicts with --skip-libs, the test drops an assertion that held on every host, and the docs name long double as a C width that differs between macOS arm64 and riscv64. The description's test results are refreshed.

Could a maintainer approve the workflow runs? They're waiting on first-time contributor approval, so target_riscv64 has only run locally so far.

[Copilot]

Copilot review overview

🟡 Changes recommended

Cross-target linking can retain host machine semantics, and exported metadata reports the wrong target.

Review effort: Balanced
Findings: 1 · 2

Open (3)

• Compile cross-target C inputs with the target machine model · New
• Test final goto binary architecture symbols and C semantics · New
• Propagate verification target into exported metadata · New

What changed in this PR

Adds experimental cross-target verification, initially supporting riscv64gc-unknown-linux-gnu.

Changes:

• Adds --target handling throughout compilation and coverage.
• Builds target-specific verification sysroots and a RISC-V machine model.
• Adds documentation and cross-target regression coverage.

File	Description
tools/​build-kani/​src/​sysroot.rs	Builds target-specific sysroots.
tools/​build-kani/​src/​parser.rs	Adds --lib-target.
tools/​build-kani/​src/​main.rs	Builds requested target libraries.
tests/​script-based-pre/​target_riscv64/​target_riscv64.sh	Exercises cross-target commands.
tests/​script-based-pre/​target_riscv64/​target_riscv64.expected	Defines expected output.
tests/​script-based-pre/​target_riscv64/​sample_crate/​src/​lib.rs	Adds RISC-V cargo test crate.
tests/​script-based-pre/​target_riscv64/​sample_crate/​Cargo.toml	Configures the test crate.
tests/​script-based-pre/​target_riscv64/​riscv64.rs	Tests RISC-V target facts.
tests/​script-based-pre/​target_riscv64/​config.yml	Configures the script test.
scripts/​kani-regression.sh	Builds RISC-V libraries in CI.
kani-driver/​src/​session.rs	Resolves target-specific libraries.
kani-driver/​src/​coverage/​cov_session.rs	Uses the verification target for coverage.
kani-driver/​src/​concrete_playback/​playback.rs	Keeps playback host-targeted.
kani-driver/​src/​call_single_file.rs	Passes targets to single-file compilation.
kani-driver/​src/​call_cargo.rs	Passes targets through Cargo.
kani-driver/​src/​args/​std_args.rs	Rejects targeted verify-std.
kani-driver/​src/​args/​mod.rs	Defines and validates --target.
kani-compiler/​src/​codegen_cprover_gotoc/​compiler_interface.rs	Adds RISC-V features and machine model.
docs/​src/​SUMMARY.md	Links the new documentation.
docs/​src/​reference/​experimental/​target.md	Documents cross-target verification.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Thanks for this. Requesting changes for two small gaps; the rest is in good shape.

I built it with cargo build-dev --lib-target riscv64gc-unknown-linux-gnu on x86_64 Linux with CBMC 6.11.0. target_riscv64, fmt, clippy and the driver/build-kani unit tests pass. Beyond the PR's test I tried a crate with a build.rs and a proc-macro dependency (the build script sees riscv64, the proc macro runs on the host), alternating host and riscv64 runs in one target dir, --coverage, autoharness on a single file, and cross-verifying for aarch64-unknown-linux-gnu from x86_64. All of those behaved. I also checked the riscv64 MachineModel against rustc's target spec, CBMC's set_arch_spec_riscv64 and the psABI, and it matches on every field.

What blocks, both inline:

• --c-lib with a non-host --target compiles the C with the host's char signedness, and I have a harness that verifies for riscv64 when it should fail. Rejecting the combination is enough for now.
• kani autoharness --std ignores --target and builds for the host. It needs the same rejection as verify-std.

With those two rejections in place (and a line each in target_riscv64), I'd approve. The other inline comments are suggestions.

On the architecture symbols in the linked .out: for Rust-only harnesses I don't think the host values make results wrong for the targets check_target accepts. Rust types reach the goto program with explicit widths and signedness, and kani_lib.c only uses size_t, uint8_t and pointers, which have the same widths on all five targets. Where it matters is C that goto-cc compiles, which is the --c-lib case. So I'm fine with precompiling kani_lib.c as a follow-up, as you proposed. I did confirm Copilot's --export-json point: the metadata says x86_64-unknown-linux-gnu for a riscv64 run, and passing verification_target() through would fix it.

On CI cost: the riscv64 library build adds about 45 s to each regression job on ubuntu-22.04. I'm fine keeping it in kani-regression.sh.

I didn't run anything on a macOS host locally (CI covers target_riscv64 there), and I couldn't do a full autoharness --std run because the std checkout I had doesn't build with this toolchain; I only checked the cargo invocation.

[feliperodri]

Soundness: --c-lib needs the same treatment as --concrete-playback here. link_goto_binary hands the --c-lib files to goto-cc, which compiles them with the host's C configuration, so C code reached from a riscv64 harness gets x86_64's signed char. Moving kani_lib.c after the Rust inputs (the follow-up from the docs thread) fixes the architecture symbols but not this, because the C functions are already typed by the time they are linked.

Reproducer on x86_64 Linux:

// cchar.c
int is_negative(char c) { return c < 0; }

// cchar.rs
use std::ffi::c_char;
extern "C" {
    fn is_negative(c: c_char) -> i32;
}

#[kani::proof]
fn char_sign() {
    let c = 200u8 as c_char;
    let r = unsafe { is_negative(c) };
    assert!(r == 1, "C saw 200 as a negative char");
}

kani cchar.rs --target riscv64gc-unknown-linux-gnu -Z unstable-options -Z c-ffi --c-lib cchar.c reports VERIFICATION:- SUCCESSFUL. On riscv64 char is unsigned, so the assertion fails there. Compiling the C file with goto-cc -funsigned-char -c cchar.c -o cu.o and passing --c-lib cu.o gives the correct FAILED.

Both flags are unstable, so rejecting --c-lib with a non-host --target is enough for this PR. Configuring goto-cc for the target can come with the kani_lib.c follow-up.

[calef]

Thanks for the reproducer. --c-lib with a non-host --target was already rejected in 1eaa2d9, with a unit test. 27bf95e adds the case to target_riscv64, using your is_negative C file, so the message a user sees is checked too. Configuring goto-cc for the target can come with a later change.

[feliperodri]

Bug: kani autoharness --std goes through the same cargo_build_std path, which now passes HOST_TARGET, but nothing rejects --target there. With kani autoharness --std <library> --target riscv64gc-unknown-linux-gnu -Z unstable-options -Z autoharness --verbose, the cargo command has --target x86_64-unknown-linux-gnu, so a successful run would be a result for the host's std while the user asked for riscv64. The same check in AutoharnessArgs::validate when self.std is set would cover it, plus a line in the test next to the verify-std one.

[calef]

Good catch, fixed in 7153afd. AutoharnessArgs::validate now refuses --target when --std is set, before the std path check, the same way verify-std does. There is a unit test covering both subcommands and a line in target_riscv64.

[feliperodri]

Suggestion: the driver accepts any string for --target and only checks whether the library folder exists, so thumbv7em-none-eabihf, x86_64-unknown-linux-musl and typos all get "build them with cargo build-dev --lib-target <triple>". For musl, following that advice fails the whole cargo build-dev with the compiler's Kani requires the target platform to be ... error, deep in the log. --target "" resolves to targets/lib. Checking the triple against the supported list here (and in build-kani for --lib-target) would give one clear error up front. A shared constant, for example in kani_metadata, would keep the driver, build-kani and check_target from drifting apart.

[calef]

Done in d67167f. SUPPORTED_TARGETS in kani_metadata is now the single list. The driver checks --target against it right after the unstable gate and lists the supported targets in the error, which covers musl, typos and --target "". build-kani checks --lib-target the same way before it builds anything. build-kani didn't depend on kani_metadata before, so that's a new path dependency for it. The compiler side is in my reply on check_target.

[feliperodri]

Suggestion: a later cargo build-dev without --lib-target leaves targets/<triple>/lib from the previous build in place, and the driver uses it. To check, I added a pub fn to library/kani/src/lib.rs and ran plain cargo build-dev: a harness calling it verified for the host and failed with E0425: cannot find function for riscv64. That's the loud case. A behavior change in library/kani or Kani's std overrides would be verified against the old copy without any error. CI always passes --lib-target, so this only affects local builds, but those are the ones where people iterate on the library. Rebuilding every target already present under targets/, or removing the folder when it isn't requested, would avoid it.

[calef]

Nice find. Done in c8a5d29: a plain cargo build-dev now rebuilds every supported target that already has a folder under targets/, as well as any named with --lib-target, and prints a line for each one it picked up. I went with rebuilding over deleting so a riscv64 setup keeps working across plain builds. --skip-libs still skips all of them.

[feliperodri]

Suggestion: now that the allowlist is meant to name exact rustc targets (the error message lists them that way), comparing session.opts.target_triple.tuple() against those five names would say so directly. The exact match on the features string is the part I'd worry about: if a toolchain bump respells it (reorders it, or lists an implied extension), riscv64 starts failing check_target. CI would catch that through the library build, so this isn't blocking.

[calef]

Done in 25e3570, using the same SUPPORTED_TARGETS list from kani_metadata. The features compare was there because riscv64gc-unknown-linux-gnu, riscv64a23-unknown-linux-gnu and riscv64-wrs-vxworks share the LLVM target riscv64-unknown-linux-gnu, and the features string was what told riscv64gc apart. The tuple does that by itself. The one thing a tuple match alone would let through is a target JSON named after a supported target, since rustc takes the tuple from the file stem, so JSON targets are refused outright.

[feliperodri]

Suggestion: kernels usually build for riscv64gc-unknown-none-elf, which check_target rejects. Verifying such a crate as riscv64gc-unknown-linux-gnu sets target_os = "linux" and makes std available, so code behind cfg(target_os = "none") is compiled out and the linux branch is verified in its place. A sentence here saying the bare-metal target isn't supported, and what changes when the Linux one stands in for it, would tell kernel users what they are and aren't verifying.

[calef]

Done in eb6c119. The page now says riscv64gc-unknown-none-elf isn't supported, and that verifying such a crate as riscv64gc-unknown-linux-gnu sets target_os = "linux" and makes std available, so cfg(target_os = "none") code is compiled out and the linux branch is what gets verified.

[calef]

Thanks for the careful review. Both blockers are in, and I took the suggestions in this PR as well rather than leaving them for later:

• 27bf95e: target_riscv64 checks the --c-lib rejection, which was already in 1eaa2d9.
• 7153afd: autoharness --std refuses --target, like verify-std.
• eb6c119: the docs say bare-metal riscv64 isn't supported and what the Linux target changes.
• d67167f: one SUPPORTED_TARGETS list, checked up front by the driver and by build-kani.
• 25e3570: check_target matches the exact tuple against that list.
• c8a5d29: cargo build-dev rebuilds every target already under targets/.

On kani_lib.c: the precompile you were fine deferring is already in 1eaa2d9, for cross targets only, so host runs keep the old goto-cc command line. And on macOS, I ran target_riscv64 on an Apple Silicon host, and the CI macOS job covers it too.

I also ran this branch against a real workload, the Kani suite of nife: 222 harnesses across 32 crates. On the host, every verdict and every CBMC formula size (program size, VCCs, properties) was identical to the PR's merge-base. With --target riscv64gc-unknown-linux-gnu the whole suite builds and verifies from macOS. For the architecture-specific code, --target from one machine reproduces what we currently need three CI jobs on two runner architectures to prove. The only difference I saw is cosmetic: the riscv64 linked program carries the separately compiled kani_lib.c prototypes with unnamed parameters.

[calef]

@feliperodri, both blockers from your review are fixed and I took the five suggestions as well; each thread has the commit that addresses it. Could you please take another look when you have a moment?

CI hasn't run here yet: the workflows from the latest push are waiting on first-time contributor approval. Could a maintainer please approve them so target_riscv64 runs on your runners?

One scope note: "Mark char as signed in the aarch64-apple-darwin machine model" changes an existing host model, not just the new target. If you'd rather review that on its own, I'm happy to split it into a separate PR.

[calef]

One more small thing: verify-std (ubuntu-22.04) in run 37961948162 timed out after 53 minutes, and the logs have since expired, so I can't tell why. Nothing in this PR touches the std verification path when --target isn't given, so I suspect it was a runner timeout. Could someone rerun that job, along with approving the pending workflows? Thanks.

[calef]

@feliperodri, a quick summary to make the re-review easy. Each of your threads has a reply naming its fix:

Your comment	Fixed in
--c-lib with a non-host --target (blocker)	rejected in 1eaa2d9 with a unit test; 27bf95e adds your is_negative case to target_riscv64
autoharness --std ignores --target (blocker)	7153afd: refused the same way as verify-std, with a unit test and a line in target_riscv64
--target accepts any string	d67167f: one SUPPORTED_TARGETS list in kani_metadata, checked by the driver and build-kani
stale targets/<triple>/lib after a plain cargo build-dev	c8a5d29: a plain build rebuilds every target already under targets/
match the exact tuple in check_target	25e3570
riscv64gc-unknown-none-elf	eb6c119: documented as unsupported, with what verifying as linux-gnu means

CI is green. I've left the threads open for you to resolve. Is there a release planned that this could make? We're carrying a patched 0.67.0 until it ships. Thanks!

[calef]

Merged main, which had moved enough to conflict. One thing to flag: #4941’s new --export-json reports target as Kani’s build triple, which is wrong under --target, so c264c69 takes it from the verification target and updates RFC 0015’s field table to match. Runs without --target report the same value as before.

CI is waiting on workflow approval for the fork. Could a maintainer approve the run when you get a chance?

[calef]

@feliperodri, this has been waiting on your re-review since the 5 October changes request. Both blockers and the five suggestions are in, each thread names its commit, and I merged main again on 26 October, so there are no conflicts. The workflows for the latest push still have not run: they need first-time contributor approval, so target_riscv64 has not run on your runners. Could you re-review, and could a maintainer approve the workflow runs? If you would rather review the "Mark char as signed in the aarch64-apple-darwin machine model" change on its own, I will split it into a separate PR. Also, is a release planned that this could make? Thank you.

[feliperodri]

@calef thanks for your patience and for the contribution. Unfortunately, I have several PRs to review for this and other repositories so this one is not yet a priority. It needs a careful review. We are also discussing about the cadence for future releases, but no actual plan for a new release at the moment.