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 be powerful in a test harness
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);
}
You have now created four accounts to make basically this post, but the point is unclear. All of the highly automated theorem provers have some limitations to what they can guarantee, some of which comically strict. You are not really explaining how this operating on MIR makes it so distinctly useless/"fraudulent".
This is really weird. Someone creating 4 new accounts just to call this project fraudulent because it can't statically analyze every property you'd like? Does this person have a personal grudge against the author, or something?
The tutorial is helpful: https://model-checking.github.io/kani/kani-tutorial.html
Reminds me a bit of hypothesis auto in its simplest applications: https://github.com/timothycrosley/hypothesis-auto/
Related. Others?
Kani Rust Verifier – a bit-precise model-checker for Rust - https://news.ycombinator.com/item?id=30786511 - March 2022 (12 comments)
Their old paper: https://dl.acm.org/doi/pdf/10.1145/3510457.3513031
A related Rust model checking tool more focused on detecting concurrency bugs: https://pure.royalholloway.ac.uk/ws/portalfiles/portal/71989...
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 be powerful in a test harness
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:
https://model-checking.github.io/kani/tutorial-first-steps.h...[dead]
[dead]
[flagged]
[flagged]
You have now created four accounts to make basically this post, but the point is unclear. All of the highly automated theorem provers have some limitations to what they can guarantee, some of which comically strict. You are not really explaining how this operating on MIR makes it so distinctly useless/"fraudulent".
This is really weird. Someone creating 4 new accounts just to call this project fraudulent because it can't statically analyze every property you'd like? Does this person have a personal grudge against the author, or something?
[flagged]
Get some help, friend. You're spiraling over the weirdest thing in the world to spiral about.
[flagged]
[dead]