Фундаментальная криптография на языке SPARK

Статья посвящена применению языка программирования SPARK для реализации фундаментальных криптографических примитивов. Рассматриваются вопросы формальной верификации и обеспечения безопасности кода, написанного на этом строго типизированном подмножестве Ada.