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
CodesInChaos 7 hours 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);
}
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".
lambda 22 hours ago [-]
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?
amazweb 22 hours ago [-]
[flagged]
SwellJoe 22 hours ago [-]
Get some help, friend. You're spiraling over the weirdest thing in the world to spiral about.
amazweb 22 hours ago [-]
[flagged]
nullsanity 22 hours ago [-]
[dead]
Rendered at 18:01:17 GMT+0000 (Coordinated Universal Time) with Vercel.
Reminds me a bit of hypothesis auto in its simplest applications: https://github.com/timothycrosley/hypothesis-auto/
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...Kani Rust Verifier – a bit-precise model-checker for Rust - https://news.ycombinator.com/item?id=30786511 - March 2022 (12 comments)