[cmarinas]

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

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.

[QuinnWilton]

This presentation is exactly the sort of thing I'm interested in, thank you!