Design of a proven correct SHA circuit
Diana Toma, A. Perez, D. Borrione, Emmanuel Bergeret · 2004
The standard SHA hash functions have been formalized, and the validity of the model has been proven correct with a mechanized theorem prover. A hardware component implementing the SHA has been designed, and proven compliant to the functional specification.