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.