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

Lessons from Verifying the range-set-blaze Crate

By Carl M. Kadie and Divyanshu Ranjan

My Rust crate range-set-blaze depends on a critical function named internal_add. The function is supposed to insert a range of integers into the crate’s data structure. But does it do so correctly? Of course, I test, but testing can miss bugs. Ideally, I want mathematical certainty of correctness.

Aside: As Rust programmers, we appreciate …

dafny formal-verification programming rust software development