I've never really worked on anything safety-critical, but I know that at least one real-time operating has been designed and verified with TLA+ [1]. The book i

I've never really worked on anything safety-critical, but I know that at least one real-time operating has been designed and verified with TLA+ [1]. The book is a bit pricey (and used copies don't pop up that often), so I haven't read it, but my understanding is that the developers felt that TLA+ did find bugs. That said, TLA+ is written separately from the code. There could of course be bugs in the translation of TLA+ -> C...TLA+ is about checking the design itself, not the code. [1] https://www.springer.com/gp/book/9781441997357 https://www.springer.com/gp/book/9781441997357