Ideally, you would like to have a specification of the system that can be translated into C and TLA+. This way it is harder to introduce bugs - it is hard to co

Ideally, you would like to have a specification of the system that can be translated into C and TLA+. This way it is harder to introduce bugs - it is hard to compile conditional or arithmetic operator differently in different places and it is trivial to do that manually. If your budget allows, it is worthwhile to invest into translation of C or TLA+ code back into specification code. This way you may run specification checks again against backtranslated specification. And you can do that process to a fixed point where nothing changes, neither (back translated) specification code, nor code generated from specification.