3 ms·

Is this only limited to (bounds|overflow|DBZ) checks? I do not know a lot about model checkers, it seems pretty cool though! and definitely something that would

• CodesInChaos 3mo ago
  The primary thing it checks for is panics. (bounds|overflow|DBZ) are just examples where Rust panics (for overflows rust doesn't always panic, while Kani always fails). You aren't testing your application code directly, but writing a test function. That test function can include any assertion you want in the end, which causes a panic, failing the verification. Similarly you want to add assumptions in the test function for pre-conditions, so parameter verification assertions in the application won't fail the verification. Example from the tutorial: #[cfg(kani)] #[kani::proof] fn verify_success() { let x: u32 = kani::any(); // estimate_size rejects x >= 4096, so this prevents failure from argument verification panicking kani::assume(x < 4096); let y = estimate_size(x); assert!(y < 10); } https://model-checking.github.io/kani/tutorial-first-steps.html https://model-checking.github.io/kani/tutorial-first-steps.h...