Source code
Revision control
Copy as Markdown
Other Tools
# SHA-2
## Verification
![verified-hacl]
This crate contains safe Rust that was compiled from verified C
> The code for [these] algorithms is formally verified using the F*
> verification framework for memory safety, functional correctness, and
> secret independence (resistance to some types of timing
> side-channels).
-- [The HACL* repository](https://github.com/hacl-star/hacl-star?tab=readme-ov-file#a-high-assurance-cryptographic-library)
For more details on the compilation from C to Rust, please refer to
["Compiling C to Safe Rust,
Jonathan Protzenko.