4 ms·
Miri: proves pre-defined properties, no changes to code other than adding a few annotations Kani: use in a test suite Creusot: annotations Verus: annotations
by gregwebs 17d ago
Miri: 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 17d 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.