Right, Frama-C can formally prove properties of C code. There are also proprietary solutions that do something similar: • https://www.eschertech.com/products/

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.eschertech.com/products/ecv.php • https://www.trust-in-soft.com/ https://www.trust-in-soft.com/