2 ms·
If you found this interesting, you may also be interested to hear about some related projects with similar goals/scopes: Miri[0], Kani[1], and Creusot[2]. There
by 63 9d ago
If you found this interesting, you may also be interested to hear about some related projects with similar goals/scopes: Miri[0], Kani[1], and Creusot[2]. There looks to be some significant overlap between Verus, Kani, and Creusot but I've not used any of them so I'll refrain from trying to differentiate them.
[0]https://github.com/rust-lang/miri https://github.com/rust-lang/miri
[1]https://github.com/model-checking/kani https://github.com/model-checking/kani
[2]https://github.com/creusot-rs/creusot https://github.com/creusot-rs/creusot
- gregwebs 9d agoMiri: proves pre-defined properties, no changes to code other than adding a few annotations Kani: use in a test suite Creusot: annotations Verus: annotations or macro The macro system looks very nice if it doesn't slow down the normal build.
- gregwebs 9d agoAI tells me that code using the verus! macro everywhere would double in build time but if only used ocassionally the verus! macro would only increase build time by a few percent. The attribute annotation would basically be free, but there is a downside that loop invariants would be rejected by stable rustc.