[qcoh]

There's a paper describing the use for railway applications [0].

A few years back I had an interesting discussion with one of its authors and was shown the real model and code. Interestingly, they generated C from the TLA+ spec and this code generator was "unproven". However, the software itself had high coverage requirements and needed to be tested extensively (100% code/branch/MCD coverage, I don't quite remember).

One of the points he made was that the upfront cost pays for itself by avoiding bugs that are hard to debug.

[0]: https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1...