PQSecure™-TRUST

Memory-safe Rust

The Rust component of the PQSecure-SW™ stack. A production-grade, memory-safe implementation of the NIST post-quantum standards for systems where memory safety and side-channel resistance are not negotiable.

Start an evaluation

Parameter sets

Standard and security level

Module Standard Level
ML-KEM-512 FIPS 203 1
ML-KEM-768 FIPS 203 3
ML-KEM-1024 FIPS 203 5
ML-DSA-44 FIPS 204 2
ML-DSA-65 FIPS 204 3
ML-DSA-87 FIPS 204 5

Algorithm coverage

The finalized NIST post-quantum standards at every parameter set, with the hash primitives hybrid deployments still depend on.

Implemented

Family and standard

Key encapsulation

  • ML-KEM-512 FIPS 203, level 1
  • ML-KEM-768 FIPS 203, level 3
  • ML-KEM-1024 FIPS 203, level 5

Digital signatures

  • ML-DSA-44 FIPS 204, level 2
  • ML-DSA-65 FIPS 204, level 3
  • ML-DSA-87 FIPS 204, level 5

Hash and auxiliary

  • SHA-3 (Keccak) FIPS 202
  • SHA-2 FIPS 180
  • HashML-DSA PreHash signing variants
  • Deterministic signing Supported

ML-KEM replaces RSA and ECDH key exchange. ML-DSA replaces RSA and ECDSA signatures.

Proven for every input, not just the tested ones

Kani is AWS's formal verification tool for Rust, running CBMC as its backend engine. It proves correctness properties mathematically, going past testing to give guarantees that hold for every possible input within defined bounds.

Two routes, one engine

libpqsecure-C is verified with CBMC directly. libpqsecure-rs reaches the same solver through Kani. Both halves of the stack answer to one proof engine.

See the full stack →

What Kani proves

  • Panic freedom No unwrap, index bounds, or division by zero, on any code path
  • Arithmetic overflow No integer operation can overflow
  • Memory safety in unsafe blocks The few unsafe boundaries are proven, not reviewed
  • Cryptographic invariants Custom assertions checked for every parameter set
  • Constant-time execution Execution independent of secret key material

One implementation, desktop to bare metal

no_std support means the verified implementation that runs on a workstation is the same one that runs on a microcontroller.

  • Target class

    Desktop and server

    Full standard library

    Linux
    x86-64
    macOS
    ARM and x86
    Windows
    Supported

  • Target class

    Embedded and MCU

    Bare-metal, no standard library

    RISC-V
    RV32 and RV64
    ARM
    Cortex-M
    Bare-metal
    no_std

Pairs with libpqsecure-asm for architecture-specific NTT and polynomial arithmetic acceleration on ARM Cortex-M4 and M33 and on RISC-V targets.

Where it goes

Built for systems where memory safety and provable correctness are requirements rather than preferences.

Engineered for

  • Memory-safe cryptographic implementation
  • Formally proven correctness
  • Embedded and bare-metal deployment
  • NIST-standardized algorithm compliance
  • Strong type enforcement at the API boundary

We combine

  • Kani formal verification
  • Rust ownership
  • Constant-time, side-channel-aware implementation
  • ACVP-tested and CAVP certified
  • Drop-in complement to libpqsecure-C

to deliver production-ready, high-assurance quantum-safe cryptography.

View the full software stack →

Certification

National Institute of Standards and Technology A7616 Cryptographic Algorithm Validation Program

Rust implementation of post-quantum cryptography algorithms with no_std support.

Validated
  • ML-KEM FIPS 203
  • ML-DSA FIPS 204
Vendor
PQSecure Technologies
View the record on NIST CSRC ↗

The C implementation is certified separately under A6936. See PQSecure-SW →

Memory-safe cryptography for mission-critical systems.

Talk with our team about integration, licensing, and embedded deployment.

Contact us