Хочется странного: найти ПО, которое по программе на C++ и её формальной спецификации скажет, соответствует ли программа спецификации. Естественно должны проверяться все выходы за пределы массива, null-pointer-dereference, переполнение чисел и т.п.

Чудес не жду, так что готов помимо спецификации программы аннотировать также и каждую функцию программы, писать всякие pre-condition, post-condition, loop variant/loop invariant. Главное, чтобы я мог написать программу, доказать её корректность, и знать, что на каждом совместимом со стандартом C++ компиляторе программа будет работать в соответствии со спецификацией (и настанет рай на земле). В крайнем случае можно сузить круг компиляторов до g++.

Аннотированная программа должна нормально компилироваться компилятором C++, а также средство верификации должно поддерживать максимально большое подмножество C++, особенно желательно STL (тут я не знаю описано ли поведение STL в стандарте C++, но если описано, то пусть прувер считает что реализация STL будет соответствовать стандарту).