В Python подготовлены криптоалгоритмы с математическим доказательством надёжности

[vened]

Верификация даёт гарантию, что программа будет выполняться только как задумали разработчики

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

Генерирование строгого кода с доказательствами - штука весьма и весьма полезная, но не очень хорошо расширять её действие до безграничного. Это больше вредит, чем помогает.

[karmael]

да честно говоря, каждая "инициатива" некрософта по "улучшению" криптоалгоритмов заканчивается truecrypt'ом

[mentin]

Преуменьшать тоже не стоит.
По крайней мере, эппловского goto fail там гарантировано быть не должно.