И всё-таки верификация не решает проблем системы и сети. Это ооочень накладно. Где-то видел шуточный селфтест: он проверял правильность того, что процедура принимала два числа и всегда возвращала ноль. Исполнение -- идеальное. Смысл? Верификация верифицировала процедуру на то, что та работает верно, результат смысла не имеет.
Опять же, как верифицировать результат при квантовых вычислениях? Это точно возможно?
Считаю подход Вирта -- строить программы в оборонительном стиле -- достаточным вместе с контрактным программированием.
Многопоточность и многопроцессность -- особенно последнее -- требует усилий. Что-то, конечно можно сделать. Даже наверное нужно (раз Дмитрий сделал).
Но важно вовремя остановиться. Чем изощрённей методика -- тем больше вероятность ошибки. А нет ничего дороже на этом свете чем глупость.