FV SHA 256

Case

File

Presentation date

Certification approved date

2023-09 FV SHA-256

2023-10-02

2025-08-04

General details

Presented by

Address

Country

Tax id

Represented by

Position

Public Name for public certified software

Formal Vindications S.L

Carrer del Bruc, 21, 2º-4ª, Barcelona

Spain

B66843327

Guillermo Errezil

Main Manager

FV SHA-256

Formally Verified Parts

File name Components Checksum
SHA256_spec.v Σ 961254744ebf0cdabff311447928818ba28475cb988f9c061828cd13db2fb0b5
sha256N.v Σ, Δ 4f8b191039e9ce5cd15a6a1e9256cce54b54a8a0db22eea84cb65d5fb6f2c86d
sha256R.v Π, Δ edba302a4cf32850e98c61f60d4668e09c3e284e8d0b617fa2a894e4d416990c
sha256U.v Π, Δ f2c77d194a70628b3c44d4d6e5f20618dbdab6385fb1a1dfa0dab9673b1fa6a4
sha256N_correct.v Π 4d07252c02c1445785293c08cdb2380ee9d0519daacd3203816c1feccd90acbb
sha256R_correct.v Π e3ca0026d37d6adcee0d97746968e8d896147f99f16fd3195afdeaa1bb17744b
sha256U_correct.v Π 7376541f289b83303eac742d854b4957aec4543f7937cd109d8630b1c63191b4
completeness.v Π 6ef02078975bb2cc15183da0c5ba5aed443f4f5136db29346ca011bd96106d1c
ssrnat_sha.v Δ 66df874c0f78c7daa2f5a160a56a57539bd10429e37f79a51dca31da7ff240b7
seq_sha.v Δ 53c4dbedf33db0af3d62ca3f08316abb1c5de6e0018b9976cdb6dc3f42aa2a4c
tail_seq.v Δ bbf8708a891faa39d7e3898a1f42bb18afc27f565eab3954e36f43ad943de13c
fi_seq_utils.v Δ d220bd417daca0e0e27fba78ab0f24cb1e8a9204da93cc022a4bdeb354d56016
uint_N.v Δ 5491ce8ce9dd2a9e3f6d51e21172ae6ebfce47e44ba588b5990e1e182db9434e
uint_utils.v Δ 5464ae824a07198ebc0c6d703c1d039ce25a2c67aba217fb3d0b2ece19460c79
sha256E.ml Λ 9bc79213b06ff83c3c9fc220afb66dfe7e2a4af8bf118089816d863c869d0ffb
sha256E.mli Λ 8d37b9a4c51a26c3a95af3515f0cb1c090cf0c598c373e16401ca3c344098f67
(*) Semi-verified until extraction verification is reached, see details on extraction.

Non Formally Verified Parts

File name Components Checksum
FV-SHA-256.fv Φ 51665ab8f58f870fca4c6ee91861935ca06763317721efb5fe13a688f7738437
FV-SHA-256Latex1.pdf Φ f09d9ad5b2ce9747804535bb984ddaa9a1a5407e2bc63dbba473704038fd0a57

Other presented parts

File name Description Checksum
sha.exe Compiled command-line interface for Windows ca2bab88e59698f6ce920c4a9a4371dd6db4a56d455e80de623fa183cc68b9bf
shae.ml Code for command-line interface, written by FV 4be525b6c6a939bbf9df3c42c9ddfd65cfde2a2c0f20ca93f0e1a64aef735655
NIST.FIPS.180-4.pdf A publication describing the standard for secure hash computation using SHA, promulgated under the provisions of FISMA, written by the US Department of Commerce together with the National Institute of Standards and Technology. 0455b406d89648d20cbde375561e19c245b9815e894164c2670772e3d54deb82