@arialdo First, use formal methods and the implementation to prove the output is always a permutation of the input.
Then, shuffle a small list a large number of times and verify the distribution is uniform. Other, more complex tests of random number generators can also be adapted and used. Since, for any finite input, repeated calls to shuffle is effectively a RNG.
Might be able to use parametricity to extend finite results to infinite lists?
Add comment