Nine Rules to Formally Validate Rust Algorithms with Dafny (Part 2)

Lessons from Verifying the range-set-blaze Crate

By Carl M. Kadie and Divyanshu Ranjan

This is Part 2 of an article formally verifying a Rust algorithm using Dafny. We look at rules 7 to 9:

• 7. Port your Real Algorithm to Dafny.
• 8. Validate the Dafny Version of Your Algorithm.
• 9. Rework Your Validation for Reliability.

See Part 1 for rules 1 to 6:

1. Don’t Learn Dafny.
2. Learn Dafny.
3. Define Your Algorithm’s Basic Concepts.
4. Specify Your Algorithm.
5. Get Help from the …

dafny formal-verification programming rust software development