But why? Tests can't catch everything. A single verified predicate is equivalent to a very large, potentially infinite number of tests.
Right now the Rust stdlib is being verified using Kani, a model checker, https://model-checking.github.io/verify-rust-std/
In Kani, a proof looks like this
https://github.com/model-checking/verify-rust-std/blob/00169...
#[kani::proof_for_contract(NonNull::new_unchecked)]
pub fn non_null_check_new_unchecked() {
let raw_ptr = kani::any::<usize>() as *mut i32;
unsafe {
let _ = NonNull::new_unchecked(raw_ptr);
}
}
It looks like a test, but actually it is testing that every possible usize, when converted to a pointer to i32 and built with NonNull::new_unchecked, will follow the contract of NonNull::new_unchecked, which is defined herehttps://github.com/model-checking/verify-rust-std/blob/00169...
#[requires(!ptr.is_null())]
#[ensures(|result| result.as_ptr() == ptr)]
Which means: if the caller guarantees that the parameter ptr is not null, then result.as_ptr() is the same as the passed ptrThat's a kind of trivial contract but Kani tests for all possible pointers (rather than some cherry picked pointers like the null pointer and something else), without actually brute-forcing them but instead recognizing when many inputs test the same thing (while still catching a bug if the code changes to handle some input differently). And this approach scales for non-trivial properties too, a lot of things in the stdlib have non-trivial invariants.
You can check out other proofs here https://github.com/search?q=repo%3Amodel-checking%2Fverify-r...
It's not that different from writing a regular test, it's just more powerful. And you can even use this #[requires] and #[ensures] syntax to test properties in regular tests if you use the https://crates.io/crates/contracts crate.
Really if you have ever used the https://proptest-rs.github.io/proptest/intro.html or the https://crates.io/crates/quickcheck crate, software verification is like writing a property test, but rather than testing N examples generated at random, it tests all possible examples at once. And it works when the space of possible examples is infinite or prohibitively large, too.
