On: Formal methods: Just good engineering practice?

[RaxcN]

I do not know TLA+, but there is an abundance of other theorem provers that can model C very closely, including overflow, assignments, etc.

So closely, that when you transcribe such an algorithm to C, there is very little room for error, even if the C code isn't proven directly.

[rramadass → RaxcN]

> there is an abundance of other theorem provers that can model C very closely

Can you list some/all of them please? Would be helpful to others here.