Prusti is a prototype verifier for Rust, built upon the the Viper verification infrastructure.
By default Prusti verifies absence of panics by proving that statements such as unreachable!() and panic!() are unreachable. Overflow checking can be enabled with a configuration flag, otherwise all integers are treated 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.
Links
- User guide
- Prusti Assistant extension for VS Code
- ETH Zürich page of the Prusti project
- GitHub repository
- Developer guide