Skip to content

HACL* + ValeCrypt + EverCrypt v0.1.0

Choose a tag to compare
@msprotz msprotz released this 02 Apr 06:05

This is the first preview release of EverCrypt, a verified cryptographic provider that offers a comprehensive selection of algorithms. EverCrypt automatically selects the best available implementation for your platform (C or assembly); offers unified APIs for families of algorithms (e.g. hashes); and its performance is on-par with what one might find in existing cryptographic libraries. In short, EverCrypt aims to deliver a verified cryptographic provider that offers the same convenience as existing, industrial-grade libraries, but with added verification guarantees.

⚠️ EverCrypt is not yet stable. The APIs will change throughout this release cycle. ⚠️

This release offers APIs for:

  • hashes (all variants of SHA2, SHA3, and for legacy, SHA1 and MD5)
  • HMAC (over SHA1, SHA2-256, SHA2-384 and SHA2-512)
  • HKDF (idem)
  • Poly1305 (both as X64 assembly and C)
  • Curve25519 (both as X64 assembly requiring BMI2 and ADX, and C)
  • AEAD ChachaPoly (C, unoptimized)
  • AEAD AES-GCM (X64 assembly requiring AES-NI)
  • Chacha20 (C, unoptimized)


  • while verification is mostly complete, a handful of small assumptions are still on the todo-list; they come with a comment explaining the gist of the assumption
  • the SHA-EXT SHA2-256 and AVX+AVX Poly1305 are currently disabled, pending further testing and verification
  • the APIs will undergo a significant revision for alpha2, including:
    • switching to C abstract structs for abstract internal states (e.g. EverCrypt_Hash_state_s)
    • offering a unified EverCrypt.Error return code
    • taking pointers as arguments whenever possible, for idiomatic C APIs
  • some un-needed copies are currently taking place and will be eliminated
  • the only algorithm for which we are making performance claims is Curve25519.

Happy hacking!