You could potentially hit your codebase with CBMC using model assertions.

Its basically what you already know in the TLA+ world but targeted against C++ code.