← All repos

libcrux

The formally verified crypto library for Rust

GitHub
cryptographyencryptionformal-verificationsignatures
Browse cluster: Lean4 Formal Verification & Cryptography →
6,117commits
53contributors
15languages

Tech stack & purpose

Libcrux is a formally verified cryptographic library written in Rust that implements a comprehensive suite of modern cryptographic algorithms including AES-GCM, ChaCha20-Poly1305, SHA-2, SHA-3, Blake2, Curve25519, Ed25519, ECDSA, RSA-PSS, HMAC, HKDF, and post-quantum algorithms like ML-KEM and ML-DSA. Many of its core algorithms are compiled from formally verified C code originating in the HACL* project, with verification performed using the F* framework for memory safety, functional correctness, and resistance to timing side-channels. The library is built in Rust with support for various platform-specific optimizations (AVX2, AES-NI, Neon instructions) and can extract implementations to C in both split-source and header-only formats, with benchmarking capabilities against third-party libraries like BoringSSL and CIRCL.

Languages

C
60.8%
Rust
20.6%
Assembly
11.0%
F*
5.2%
C++
1.2%
Python
0.5%
Shell
0.2%
Lean
0.2%
CMake
0.1%
Makefile
0.1%
Nix
0.1%
HTML
0.1%
Go
0.0%
Dockerfile
0.0%
sed
0.0%

Contributors (top 30 of 53)