Формальная верификация ПО

Для повышения надёжности ключевые элементы компьютерной инфраструктуры должны быть формально верифицированы т.е. для них должно быть сделано математическое доказательство того, что они соответствуют требованиям, проверка самих требований это отдельный вопрос, но эту задачу обычно решают лучше чем реализацию. Верификация это не решение всех проблем, но это наиболее надёжный метод создания ПО из доступных нам, который позволяет быть уверенным, что реализация соответствует требованиям, ведь чаще всего ошибки именно в реализации. Таким образом мы сможем сделать иерархию надёжных компонентов, в которой каждый следующий будет опираться на надёжные предыдущие. Подробнее в отдельной статье [verify].