The authors have posted a follow-up posting: about KeY - the tool used to prove the bug in TimSort - http://envisage-project.eu/key-deductive-verification-of-sof...