> но не поможет «покончить с уязвимостями раз и навсегда».

А давайте тогда без передерга или хотя бы развернуто, а? А то можно сразу Тюринга и "проблему остановки" упомянуть, больше ничего и не надо.

Вообще-то, речь шла о "свести наличие уязвимостей к нулю".

Кстати, моделирование и описание логики на высоком уровне (мат-модель) и последующая реализация на более "низком" очень неплохо помогает отлавливать логические ошибки типа "хотел сделать то, но на самом деле сделал вот это" даже одному разработчику (потому что задача формулируется на двух разных языках, шанс что мозг "прокеширует" и "замылится" на одной и той же детали, соотв. ниже).

Так же, в ожидании очередного "верификация не поможет от всего поэтому: Нинужно" специально было процитировано из Abstract "a system is free of programming errors" (ошибки в логике, это  "logic errors" и идут отдельным пунктом).

хотя  из интересного там вообще вот это:
> the formal verification has uncovered another 144 defects  and resulted in 54 further changes to the code to aid in the proof.
> None of the bugs found in the C verification stage were deep in the sense that the corresponding algorithm was flawed. This is because the C code was written according to a very precise, low-level specification which was already verified in the first refinement stage.
> Algorithmic bugs found in the first stage were mainly missing checks on user assumptions
>  The bugs discovered in the second proof from executable spec to C were mainly typos, misreading the specification, or failing to update all relevant code parts for specification changes. Simple typos also made up a surprisingly large fraction of discovered

Т.е. нашли 144 ошибки на 8000 строк кода, причем алгоритмические и прочие "высокоуровневые" ошибки ловоились еще до написания С кода, во время рефайнмента.
Вряд ли обычный, неверифицируемый код сильно отличается, плюс там еще и спецификацию никто не проверяет.