4 ms·
Kani: A Model Checker for Rust
- ototot 4mo agoTheir old paper: https://dl.acm.org/doi/pdf/10.1145/3510457.3513031 https://dl.acm.org/doi/pdf/10.1145/3510457.3513031
- ZeroCool2u 4mo agoThe tutorial is helpful: https://model-checking.github.io/kani/kani-tutorial.html 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/ https://github.com/timothycrosley/hypothesis-auto/
- deleted 4mo ago[deleted]
- yusofake 4mo ago[dead]
- deleted 4mo ago[deleted]
- utterfake 4mo ago[flagged]
- bestonetwo 4mo ago[dead]
- amazweb 4mo ago[flagged]
- jchw 4mo agoYou 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".
- SwellJoe 4mo agoGet some help, friend. You're spiraling over the weirdest thing in the world to spiral about.
- amazweb 4mo ago[flagged]
- nullsanity 4mo ago[dead]
- rando1234 4mo agoA related Rust model checking tool more focused on detecting concurrency bugs: https://pure.royalholloway.ac.uk/ws/portalfiles/portal/71989788/rustmc_paper.pdf https://pure.royalholloway.ac.uk/ws/portalfiles/portal/71989...
- dang 4mo agoRelated. Others? Kani Rust Verifier – a bit-precise model-checker for Rust - https://news.ycombinator.com/item?id=30786511 https://news.ycombinator.com/item?id=30786511 - March 2022 (12 comments)
- ramon156 4mo agoIs 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 4mo agoThe 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...