EverCrypt is a formally verified modern cryptographic provider that provides cross-platform support as well as platform-specific optimizations that are automatically enabled if processor support is detected (multiplexing). Furthermore, EverCrypt offers an (agile) API that makes it simple to switch between algorithms (e.g., from SHA2 to SHA3).

EverCrypt is written and verified using the F* programming language, then compiled to a mixture of C (using a dedicated compiler, KreMLin) and assembly.

EverCrypt's formal verification involves using software tools to analyze all possible behaviors of a program and prove mathematically that they comply with the code's specification (i.e., a machine-readable description of the developer's intentions). Unlike software testing, formal verification provides strong guarantees that a program behaves as expected and is free from entire classes of errors.
Portions of EverCrypt are being used in Firefox, the Windows kernel, the Tezos blockchain, and the Wireguard VPN.