diff --git a/data/tools/kani.yml b/data/tools/kani.yml new file mode 100644 index 0000000000..b289bfa838 --- /dev/null +++ b/data/tools/kani.yml @@ -0,0 +1,19 @@ +name: kani +categories: + - wasd +tags: + - rust + - Security/SAST +license: 'MIT & Apache 2.0' +source: 'https://github.com/model-checking/kani' +homepage: 'https://github.com/model-checking/kani' +description: >- + The Kani Rust Verifier is a bit-precise model checker for Rust. + Kani is particularly useful for verifying unsafe code blocks in Rust, + where the "unsafe superpowers" are unchecked by the compiler. + Kani verifies: + + * Memory safety (e.g., null pointer dereferences) + * User-specified assertions (i.e., assert!(...)) + * The absence of panics (e.g., unwrap() on None values) + * The absence of some types of unexpected behavior (e.g., arithmetic overflows)