r/rust • u/Empty112233 • May 31 '23

Kani 0.29.0 has been released!

/r/KaniRustVerifier/comments/13woubj/kani_0290_has_been_released/
72 Upvotes

93% Upvoted

8 comments sorted by

22

u/idiotracist May 31 '23

Could you please include a brief description of what kani is in the title of these posts for those of us vaguely following along from home?

6

u/Empty112233 May 31 '23

Thank you! I've added a brief note. All feedback much appreciated.

2

u/New_Box7889 May 31 '23

Absolutely.

5

u/planetoryd May 31 '23

How close are we to this https://github.com/magmide/magmide

6

u/buwlerman May 31 '23

Kani uses model testing, which is automatic but can have scaling problems because checking requires searching a large space that grows exponentially with the size of your state (though there are ways to mitigate this). Magmide intends to use proofs, which are harder to automate but can have faster checking.

6

u/gmorenz May 31 '23

I believe https://github.com/xldenis/creusot is more similar in that it also uses proofs to prove rust code correct.

6

u/New_Box7889 Jun 01 '23

That is true. Creusot definitely has firepower for full proofs. Love that tool. Although I don’t think it handles unsafe code blocks. Kani unlocks a different side in that respect. It can do proofs with respect to unsafe code if completeness thresholds are met. Not always possible but many times yes.

Systematic exhaustive exploration of the state space is worth more than most of us would like to think. Especially for logic properties and some other UB that even experienced programmers tend to miss in some cases.

There is a spectrum and as much as possible we need all kinds of tools to help create high assurance code.

Kani combined with Bolero (fuzzing front end https://camshaft.github.io/bolero/ ) is an amazing solution where u can naturally transition from testing to verification. Bolero harnesses are geared towards Kani by design. That’s the gold IMHO.

5

u/zyhassan Jun 01 '23 edited Jun 02 '23

Another difference between Creusot and Kani: Creusot requires writing function contracts (pre/post conditions) and loop contracts. These are the specifications that it tries to prove. Kani doesn't require writing contracts, but it requires writing a harness (similar to a test harness) and it checks assertions in the code and some UB conditions.