I used it in the context of Linux kernel development to model/verify various algorithms. I gave a presentation last year at Linux Plumbers: http://procode.org/

I used it in the context of Linux kernel development to model/verify various algorithms. I gave a presentation last year at Linux Plumbers: http://procode.org/FormalMethodsPlumbers2018.pdf http://procode.org/FormalMethodsPlumbers2018.pdf Slides 4 and 28 list actual bugs found by such modelling. I do find TLA+ (or formal modelling in general) pretty useful for real world cases, only that, unfortunately, I don't always have the time.