Prusti is a verifier for the Rust language based on permission logic and using the Viper verifier as an intermediate verification language. Prusti was developed by ETH Zurich.

An unusual part of its design is that it makes use of magic wands to model reference borrowing.

Notes related to Prusti verifier

Ownership types, Prusti verifier, Rust language, Viper verifier

Papers related to Prusti verifier

• Verifying safe clients of unsafe code and trait implementations in Rust [beckmann:msc:2020]
• Witnessing the elimination of magic wands [blom:ijsttt:2015]
• Extended support for borrowing and lifetimes in Prusti [gorse:msc:2020]
• Lightweight support for magic wands in an automatic verifier [schwerhoff:ecoop:2015]