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 rea

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/1rAn3N5hViv3xNe2E55lMzpFFym1lpx9C/view https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1...