А ведь могли бы взять frama-c, если так заботятся о "memory safety" и верифицировали свой говнокод.
Криптография, кста, отлично верифицируется. Ибо спецификация не содержит двухзнаычных трактовок и всё достаточно просто.
Но нет. Всем похуй. Тащим раст потому, что это модно.