Verifying the Fisher-Yates Shuffle Algorithm in Dafny

This conference talk presents a verification of the Fisher-Yates shuffle algorithm using the Dafny programming language. Learn how researchers from Amazon Web Services establish the correctness of this popular shuffling algorithm that generates uniformly random permutations. Follow their three-step verification approach: defining a functional model using sequences and random bit streams, proving the model produces the desired distribution, and creating an imperative implementation with arrays that's equivalent to the functional model. Discover how implementation errors can introduce bias into shuffled sequences and how formal verification helps prevent these issues. The 18-minute presentation from the Dafny 2025 workshop offers a verification blueprint that can be applied to more complex algorithms.