Глядя на C, C имеет хорошую поддержку формальных методов, которые могут использоваться в коде (frama-c, VCC, verifast). Насколько мне известно, С++, похоже, не сопоставим.
Какие формальные методы доступны для рассуждений о критическом для безопасности программном обеспечении, написанном на С++?
Медицинская компания, с которой я работаю, использует Coverity и Klocwork, чтобы проверить код на возможные проблемы, такие как утечки ресурсов и неинициализированный указатель, который будет использоваться.
Однако, это инструменты, а не стандартные для критического кода безопасности.
То, что я видел, это то, что MISRA работает над стандартом для С++. Они начали с C обратно, и начали работать на С++ около 5 лет назад или около того. Одна большая проблема заключается в том, что стандарт MISRA для С++, например, говорит, что вы не должны использовать шаблоны. Это действительно ограничивает то, что вы можете сделать на С++. Однако вы можете использовать этот документ в качестве отправной точки. Вы можете ограничить шаблоны, используемые в вашем программном обеспечении, тем, что входит в стандартную библиотеку и, например, повысить.
Обратите внимание, что Klocwork имеет расширение для MISRA С++.
Тем не менее, один из лучших способов написать хороший код - проверить его с помощью модульных тестов и тестов интеграции. Я нашел с годами, что это намного надежнее, чем большинство других методов.