3 releases

0.0.2-beta.3 Feb 24, 2025
0.0.2-alpha.3 Jul 23, 2024
0.0.2-alpha.1 Jul 3, 2024

#1812 in Cryptography

Download history 98/week @ 2024-11-18 168/week @ 2024-11-25 72/week @ 2024-12-02 114/week @ 2024-12-09 229/week @ 2024-12-16 21/week @ 2024-12-30 183/week @ 2025-01-06 279/week @ 2025-01-13 299/week @ 2025-01-20 101/week @ 2025-01-27 153/week @ 2025-02-03 71/week @ 2025-02-10 126/week @ 2025-02-17 253/week @ 2025-02-24 254/week @ 2025-03-03

704 downloads per month
Used in 4 crates (via libcrux-psq)

Apache-2.0

590KB
10K SLoC

HKDF

Verification

verified-hacl

This crate contains safe Rust that was compiled from verified C originating in the HACL* project.

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

For more details on the compilation from C to Rust, please refer to "Compiling C to Safe Rust, Formalized" by Aymeric Fromherz and Jonathan Protzenko.

Dependencies

~1.3–1.9MB
~32K SLoC