Verification Features
Even if no specifications are provided, Prusti is capable of verifying a few basic properties about the supplied Rust code. These properties include:
More intricate properties require users to write suitable specifications. The following features are either currently supported or planned to be supported in Prusti:
- Pre- and postconditions
- Assertions, refutations and assumptions
- Trusted functions
- Pure functions
- Predicates
- External specifications
- Loop body invariants
- Pledges
- Type-conditional spec refinements
- Closures
- Specification entailments
- Type models
- Conditional compilation
By default, Prusti only checks absence of panics. Moreover, Prusti verifies partial correctness. That is, it only verifies that terminating program executions meet the supplied specification.