[grandpa]

There's a difference, though: QuickCheck randomly tries a large-ish number of possible inputs to try and disprove a postcondition, whereas formal methods prove the postcondition for all inputs. Practically, if the number of possible inputs is huge compared to the number of failure cases, it's unlikely that QuickCheck will find it. I strongly suspect - and this would be an interesting experiment - that QuickCheck wouldn't have found this particular bug, since Timsort has been in use for years without anyone noticing it.

[TheLoneWolfling]

What about AFL?

[jamesfisher]

What's AFL?

[fpgaminer]

American Fuzzy Lop (http://lcamtuf.coredump.cx/afl/), a fuzzer which instruments programs at compile-time to help find interesting inputs faster than brute-force fuzzing.

It may have indeed found a bug in TimSort, since it's more apt at exercising branches, but I think AFL is C/C++ only.