rust verification tools
2022-01-13 · 1 min read
Rudra is a static analyzer to detect common undefined behaviors in Rust programs. It is capable of analyzing single Rust packages as well as all the packages on crates.io.
By default Prusti verifies absence of integer overflows and panics by proving that statements such as
panic!() are unreachable. Overflow checking can be disabled with a configuration flag, treating all integers as unbounded. In Prusti, the functional behaviour of a function can be specified by using annotations, among which are preconditions, postconditions, and loop invariants. The tool checks them, reporting error messages when the code does not adhere to the provided specification.