For instance, see this recent post about using TLA+ to find a concurrency bug in glibc's implementation of pthreads:

https://probablydance.com/2020/10/31/using-tla-in-the-real-w...