SHA-256 is a cryptographic hash function designed by the United States National Security Agency (NSA) and published in the FIPS PUB 180-2 standard. It produces a 256-bit hash value and is widely used due to its high security strength

The FormalV team offers a formally verified version of the algorithm for higher security. This software is built according the (4+1)-tuple method for Public Certification of a Specification and its Software. The main issue encountered while developing this project was the low efficiency of the extracted verified code. However, several optimizations have allowed us to provide a version fast enough for our industrial purposes.