[MaxBarraclough]

Right, Frama-C can formally prove properties of C code.

There are also proprietary solutions that do something similar:

• https://www.eschertech.com/products/ecv.php

• https://www.trust-in-soft.com/