Using TLA+ in the Real World to Understand a Glibc Bug

made by Malte Skarupke, submitted by nicholasbs
A detailed analysis of using TLA+ to solve a bug in complex, real-world code.