9 releases

0.0.4 Nov 5, 2025
0.0.3 Jul 1, 2025
0.0.3-alpha.3 Jun 23, 2025
0.0.3-alpha.1 May 26, 2025
0.0.2-beta.3 Feb 24, 2025

#2491 in Cryptography

Download history 5896/week @ 2025-10-17 2955/week @ 2025-10-24 6676/week @ 2025-10-31 6151/week @ 2025-11-07 5843/week @ 2025-11-14 7530/week @ 2025-11-21 5139/week @ 2025-11-28 7690/week @ 2025-12-05 5681/week @ 2025-12-12 2817/week @ 2025-12-19 2978/week @ 2025-12-26 3954/week @ 2026-01-02 6773/week @ 2026-01-09 7703/week @ 2026-01-16 5933/week @ 2026-01-23 7788/week @ 2026-01-30

29,015 downloads per month
Used in 3 crates (via libcrux-chacha20poly1305)

Apache-2.0

535KB
9K SLoC

Poly1305

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

~135–530KB
~12K SLoC