Tim Peters developed the Timsort hybrid sorting algorithm in 2002. TimSort is today used as the default sorting algorithm for Android SDK, Sun’s JDK, OpenJDK, Python, Apache, Hadoop and many other languages and rameworks. Given the popularity of these platforms, the number of computers, cloud services and mobile phones that use TimSort for sorting is well into the billions.
Fast forward to 2015. After we had successfully verified Counting and Radix sort implementations in Java with a formal verification tool called KeY, we were looking for a new challenge. TimSort seemed to be the ideal candidate for several reasons: it is rather complex, widely used, had a bug history but was reported as fixed in Java 8, and was extensively tested. Unfortunately, we weren’t able to prove its correctness. A closer analysis showed that this was, quite simply, because TimSort was broken and our theoretical considerations finally led us to a path towards finding the bug. We show how we did it, derive a mechanically verified bug-free version and discuss the reactions of the developer communities involved in the implementation of the Java and Python standard libraries.