You don't validate the C++ code, you validate the algorithm before you implement it with C++.

You have an idea for an algorithm, write it down with TLA+.

TLA+ tells you if you screwed something up.

You refine the algorithm until TLA+ says it's okay now.

You implement the refined algorithm with the programming language of your choice.

Everything that happens from that point is outside of TLA+'s power.