High Assurance Cryptography
We provide tools, software, and services to increase trust into your most critical systems.
We provide tools, software, and services to increase trust into your most critical systems.
We design cryptography based security solutions with rigorous formalism. We write design specifications, architect solutions, answer your questions to anything from encryption to authentication.
We prove that your systems meet security, safety, and privacy goals. We write rigorous system specification and perform security and correctness proofs.
We implement high assurance software for security critical components. We write security critical code, use formally verified components, and allow for formal verification of the entire system.
HACL packages is a collection of cryptographic libraries developed by Cryspen on top of HACL* in C, Rust, OCaml, and JavaScript.
Learn morehacspec is a specification language for cryptography in Rust. An easy way for anyone to get started with formally verifying cryptography.
Learn more
OpenMLS is an implementation of the Messaging Layer Security (MLS), a building block to implement end-to-end encrypted applications.
Learn moreCIRCUS is a toolchain to build high assurance software products. It allows security analysis and full functional verification.
Learn moreHybrid public key encryption (HPKE - RFC 9180) is a variant of public key encryption of arbitrary-sized plaintexts for a recipient public key.
Learn more