Formal verification of a Streebog hash function implementation with the Astra Group

Ensuring trust in cryptographically secure algorithm implementations is a relevant task in modern programming. Because increased correctness requirements are imposed on such software systems, the proof of their correctness with respect to a certain formal specification is constructed via deductive verification. This article outlines the progress made towards the proof of correctness of the Streebog hash function implementation located in the Linux kernel with respect to the GOST R 34.11-2012 standard. The work began as part of the "Formal verification of a Streebog hash function implementation with the Astra Group" project during the 2025 Great Mathematical Workshop. As the result of our work we present a formalization of the GOST R 34.11-2012 algorithm in the Rocq proof assistant's Gallina language. This formalization can serve as a functional specification for any implementation of the Streebog hash function. We also present specifications for some of the basic functions present in the Streebog hash function implementation located in the Linux kernel and also methods of simplifying proofs of correctness of such functions by formulating lemmata that establish a correspondence between the data structures present in the implementation and the data structures outlined in the functional specification.