4 ms·
Another cool tool that’s being developed for rust is verus. It’s not the same as Kani and is more of a fork of the rust compiler but it lets you do some cool ve
by nomadygnt 10mo ago
Another cool tool that’s being developed for rust is verus. It’s not the same as Kani and is more of a fork of the rust compiler but it lets you do some cool verification proofs combined with the z3 SMT solver. It’s really a cool system for verified programs.
- rocqua 10mo agoI had a look, and it seems cool. But it doesn't seem to do the thing I love about Kani: work with only very partial annotations, only proving the annotations and being a very light lift on code not relevant for the annotations.