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:

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.