kani
kani copied to clipboard
model-checking
Kani Rust Verifier
#4127 turned on some target features on some platforms (e.g. `sse` and `sse2` on x86_64 and `neon` on aarch64). One of the regressions suffered a significant slowdown as a result...
This PR is not ready for review; I am testing that it passes CI before writing tests. Resolves #ISSUE-NUMBER By submitting this pull request, I confirm that my contribution is...
This is a tracking issue for fixing the [known quantifiers limitation](https://model-checking.github.io/kani/reference/experimental/quantifiers.html#types-of-quantified-variables) that the ranges must be usizes. I tried this code: ```rust #[kani::requires(min != 0 && max != 0)] #[kani::ensures(|result|...
I tried this code: ```rust// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use std::mem; extern crate kani; use kani::{kani_exists, kani_forall}; #[kani::proof] fn main() { let original_v = vec![kani::any::(); 3];...
Requested feature: Users should be able to easily stub code that they expect to be unreachable from a harness in order to accelerate verification. Use case: In some cases, such...
Assess further compounded an already existing issue that we'll need to address before it gets too much worse. Here are a few known issues, in no particular order: * [...
I was attempting to write harnesses for trait method implementations in verify-rust-std, but I could not get Kani to resolve the qualified path of the function. I tried this code...
Document the experimental list subcommand feature in our book and stabilize the feature.
I was following [the instructions to run Kani on the verify-rust-std project](https://model-checking.github.io/verify-rust-std/tools/kani.html#using-kani-to-verify-the-rust-standard-library), and everytime I execute the command the entire project gets rebuilt, even when there are no changes to...
**Requested feature:** I believe Kani can take advantage of [RUSTC_WRAPPER_WORKSPACE](https://doc.rust-lang.org/cargo/reference/environment-variables.html) environmental variable to implement compilation of all crates in a workspace in a single pass improving compilation times. Use case:...