Kani: A Model Checker for Rust

https://arxiv.org/abs/2607.01504

by Jimmc414 • 16 days ago

160 6 16 days ago

arxiv.org

ototot• 16 days ago

Their old paper: https://dl.acm.org/doi/pdf/10.1145/3510457.3513031

ZeroCool2u• 16 days ago

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/

rando1234• 16 days ago

A related Rust model checking tool more focused on detecting concurrency bugs: https://pure.royalholloway.ac.uk/ws/portalfiles/portal/71989...

dang• 16 days ago

Related. Others?

Kani Rust Verifier – a bit-precise model-checker for Rust - https://news.ycombinator.com/item?id=30786511 - March 2022 (12 comments)

ramon156• 16 days ago

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• 16 days 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.h...

Kani: A Model Checker for Rust

Related Stories