Functional verification with mechanical proofs of TimSort [pdf]

Key result: there's a bug in Java's library sort. It takes a sort of 6710886 chosen elements to force it, which will force a subscript out of range.