4 releases

new 0.0.3-alpha.2 Jun 12, 2025
0.0.3-alpha.1 May 26, 2025
0.0.2 Mar 25, 2025
0.0.2-beta.3 Feb 24, 2025

#2812 in Cryptography

Download history 103/week @ 2025-02-19 33/week @ 2025-02-26 19/week @ 2025-03-05 195/week @ 2025-03-19 103/week @ 2025-03-26 317/week @ 2025-04-02 318/week @ 2025-04-09 85/week @ 2025-04-16 158/week @ 2025-04-23 239/week @ 2025-04-30 72/week @ 2025-05-07 480/week @ 2025-05-14 290/week @ 2025-05-21 441/week @ 2025-05-28 572/week @ 2025-06-04

1,805 downloads per month
Used in 2 crates

Apache-2.0

585KB
10K SLoC

Chacha20-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.

NOTE: The XChacha20Poly1305 wrapper has not been formally verified yet.

Dependencies

~190–620KB
~15K SLoC