Even More Bugs in Cryspen’s libcrux: ML-DSA

Over the past two weeks, we have published eight vulnerabilities across Cryspen’s cryptographic libraries, including three bugs in formally verified code that Cryspen’s own documentation claims is correct.

We now report three additional findings in libcrux’s ML-DSA implementation—the post-quantum digital signature algorithm standardized as FIPS 204. The first two are FIPS 204 specification violations in runtime code. The third is a wrong specification in the F* formal verification infrastructure that renders AVX2 proofs unsound.

Update (Feb 19): Finding 3 added—an error in the ML-DSA AVX2 proof specification that makes the formally verified intrinsics axioms logically false.

Update (Mar 6): Cryspen has fixed Findings 1 and 2. Finding 1 (verifier norm check) was fixed in PR #1347, merged March 4, 2026. Finding 2 (hint deserialization) was fixed in PR #1348, merged March 4, 2026. Both PRs credit the discoverer.

Finding 1: ML-DSA Verifier Norm Check Is Dead Code

Location: libcrux-ml-dsa/src/ml_dsa_generic.rs, line 404.

The ML-DSA verifier checks whether the signer response vector $\mathbf{z}$ has an infinity norm below a certain bound. This is a critical security check: it ensures that $\mathbf{z}$ does not leak information about the secret key. FIPS 204, Algorithm 8 (ML-DSA.Verify_internal), step 13 specifies:

And Algorithm 7 (ML-DSA.Sign_internal), step 23 specifies:

Both use $\gamma_1 - \beta$. The libcrux verifier uses the wrong bound:

// Line 402-405 (verifier, BUG):
if vector_infinity_norm_exceeds::<SIMDUnit>(
    &deserialized_signer_response,
    (2 << GAMMA1_EXPONENT) - BETA,
//   ^^^^^^^^^^^^^^^^^^^^^^^^ = 2·γ₁ - β
) {
    return Err(VerificationError::SignerResponseExceedsBoundError);
}

The expression 2 << GAMMA1_EXPONENT computes $2 \cdot 2^{\gamma_1\text{exp}} = 2\gamma_1$, not $\gamma_1$. Compare with the signer, which correctly uses 1 << GAMMA1_EXPONENT:

// Line 284 (signer, correct):
if vector_infinity_norm_exceeds::<SIMDUnit>(&mask, (1 << GAMMA1_EXPONENT) - BETA) {
//                                                  ^^^^^^^^^^^^^^^^^^^^^^^^ = γ₁ - β

The signer checks $\gamma_1 - \beta$. The verifier checks $2\gamma_1 - \beta$. One constant was doubled.

The Check Can Never Trigger

The signer response $\mathbf{z}$ is deserialized from a $\gamma_1$-encoded representation: each coefficient is encoded as a value in $[-\gamma_1, \gamma_1]$. This means that for any deserialized $\mathbf{z}$, $\lVert\mathbf{z}\rVert_\infty \leq \gamma_1$. The buggy bound is $2\gamma_1 - \beta$. Since $\beta > 0$:

The check vector_infinity_norm_exceeds(&deserialized_signer_response, (2 << GAMMA1_EXPONENT) - BETA) can never return true. The verifier’s norm check is dead code. For each ML-DSA parameter set:

In every case, the maximum possible infinity norm ($\gamma_1$) is less than the buggy bound ($2\gamma_1 - \beta$). The check is vacuously true. The verifier unconditionally passes any deserialized signer response, regardless of whether it satisfies the FIPS 204 requirement $\lVert\mathbf{z}\rVert_\infty < \gamma_1 - \beta$.

Concrete Impact

A conforming signer will never produce a signature with $\lVert\mathbf{z}\rVert_\infty \geq \gamma_1 - \beta$—the signing algorithm rejects such candidates and retries. But a malicious signer could produce signatures with $\gamma_1 - \beta \leq \lVert\mathbf{z}\rVert_\infty \leq \gamma_1$ that pass libcrux’s verifier but would be correctly rejected by any FIPS 204-conforming implementation.

This creates an interoperability hazard. A system using libcrux for verification would accept signatures that every other conforming implementation rejects:

• Post-quantum certificate chains. A certificate authority or TLS implementation using libcrux to verify ML-DSA signatures on certificates would accept certificates that conforming verifiers reject. An attacker could issue a certificate that appears valid to libcrux-based systems but is rejected everywhere else, creating a split view of the PKI.
• Firmware signing. A secure boot chain using libcrux for signature verification would accept firmware images signed with out-of-bound $\mathbf{z}$ vectors. A malicious firmware image could pass libcrux’s verification while being correctly rejected by any other FIPS 204-conforming verifier on the same device or in audit tooling.
• Consensus protocols. In a distributed system where nodes verify ML-DSA signatures to reach agreement, libcrux nodes would accept messages that non-libcrux nodes reject. An adversary could exploit this to partition the network: libcrux nodes see a valid message, conforming nodes do not.

Provenance

Introduced in commit 326c837a33 on January 7, 2025, by Jonas Schneider-Bensch, with the message “Further macro monomorphization of parameter sets.” The signer’s correct bound was already present in the codebase. The verifier’s bound was written incorrectly in the same refactoring pass.

Finding 2: Hint Deserialization Missing Final Bound Check

Location: libcrux-ml-dsa/src/encoding/signature.rs, lines 91–120.

ML-DSA signatures contain a hint vector $\mathbf{h}$ that encodes which coefficients of the high-order bits need adjustment. The hint is serialized as a list of indices followed by cumulative counts, with a maximum of $\omega$ total true hints across all polynomials. FIPS 204, Algorithm 21 (HintBitUnpack), step 4 specifies, for every row $i$ from 0 to $k - 1$:

This checks the current cumulative count $y[\omega + i]$ against $\omega$ on every iteration. It ensures that no row’s cumulative count exceeds the allowed maximum.

The libcrux implementation checks the wrong variable:

for i in 0..rows_in_a {
    let current_true_hints_seen = hint_serialized[max_ones_in_hint + i] as usize;

    if (current_true_hints_seen < previous_true_hints_seen)
        || (previous_true_hints_seen > max_ones_in_hint)
    //      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    //      Checks PREVIOUS iteration's count, not current.
    //      FIPS 204 checks: y[ω + i] > ω (i.e., current > max)
    {
        malformed_hint = true;
        break;
    }

    for j in previous_true_hints_seen..current_true_hints_seen {
        // ... process hint indices ...
        set_hint(out_hint, i, hint_serialized[j] as usize);
    }

    // ...
    previous_true_hints_seen = current_true_hints_seen;
}

The check uses previous_true_hints_seen > max_ones_in_hint instead of current_true_hints_seen > max_ones_in_hint. It validates the count from the previous iteration rather than the current one. For the last row (i = rows_in_a - 1), the current count is read, the hint indices are processed and applied via set_hint, and previous_true_hints_seen is updated—but the overflow check will not fire until the next iteration, which never comes.

The subsequent padding check (line 122) is supposed to verify that all remaining bytes in the hint section are zero:

for j in previous_true_hints_seen..max_ones_in_hint {
    if hint_serialized[j] != 0 {
        malformed_hint = true;
        break;
    }
}

But if previous_true_hints_seen equals or exceeds max_ones_in_hint after the last row, this range is empty and the loop body never executes. The padding check is silently skipped.

Concrete Impact

A crafted signature can set the last row’s cumulative count to a value greater than $\omega$ (max_ones_in_hint). The inner loop will then iterate over bytes in the trailer region of the hint encoding, interpreting arbitrary byte values as hint indices and setting corresponding positions via set_hint. For each parameter set:

The trailer bytes are the cumulative count bytes for each row. An attacker controls these values as part of the signature. By setting the last row’s count to max_ones_in_hint + rows_in_a (or any value up to 255), the inner loop reads the trailer bytes as hint indices, setting arbitrary hint positions in the last polynomial. This produces a hint vector that a FIPS 204-conforming implementation would reject.

As with the verifier norm bound, this creates a divergence between libcrux and conforming implementations. A signature accepted by libcrux may be rejected elsewhere, or worse, the corrupted hint vector may cause the verification to produce a different result than intended:

• Signature forgery assistance. The hint vector directly affects which high-order bits are adjusted during verification. By injecting arbitrary hint positions through the overflow, an attacker gains additional degrees of freedom in crafting signatures that pass verification. This weakens the effective security of the scheme by relaxing constraints that the signer is supposed to satisfy.
• Cross-implementation disagreement. A signature with an overflowed hint count would verify successfully under libcrux but fail under any conforming implementation. In a system where multiple parties independently verify the same signature—such as a transparency log or a multi-verifier protocol—this produces contradictory verification results with no indication of which is correct.
• Strong unforgeability violation. FIPS 204 mandates a unique hint encoding precisely to ensure strong unforgeability: each valid signature has exactly one valid serialization. The missing bound check allows multiple distinct serializations to decode to the same logical signature, breaking this property. An attacker can produce a second valid encoding of an existing signature without access to the signing key.

Provenance

The hint deserialization logic has been touched by multiple authors across several commits. The current loop structure was established by Jonas Schneider-Bensch in commit 83ffae727d on January 2, 2025, and further modified by Franziskus Kiefer (Cryspen’s CEO) in commit 404115bc08 on January 13, 2025. The early-return logic was later replaced with flag-and-break by Jonas Schneider-Bensch in commit d979b001f9 on November 17, 2025, as a workaround for a bug in Eurydice, with the comment: “We would like to use early returns below, but doing so triggers a bug in Eurydice.”

The workaround for Eurydice’s inability to handle early returns inside loops restructured the control flow in a way that obscured the missing final bound check. The original early-return code may or may not have had the same bug, but the flag-and-break rewrite made it harder to spot.

Finding 3: Wrong Multiplication Specification in ML-DSA AVX2 Proofs

Location: libcrux-ml-dsa/proofs/fstar/spec/Spec.Intrinsics.fsti, line 97.

The F* specification file Spec.Intrinsics.fsti defines the semantics of low-level AVX2 intrinsics used in the ML-DSA proof infrastructure. The function i16_mul_32extended specifies 16-to-32-bit widening multiplication—the primitive underlying Intel’s VPMADDWD and VPMULLW instructions. It takes two parameters x and y:

[@@ "opaque_to_smt"]
let i16_mul_32extended (x y: i16): i32 =
  (cast x <: i32) *! (cast x <: i32)
(*               ^^^ should be: cast y *)

The body uses x for both operands. The parameter y is completely ignored. The function computes $x^2$ instead of $x \cdot y$. This is likely a copy-paste error: cast x was duplicated instead of writing cast y for the second operand.

Why Formal Verification Cannot Catch This

Three mechanisms conspire to make this bug invisible to the F* proof system:

1. The definition is hidden from the solver. The [@@ "opaque_to_smt"] attribute on line 96 prevents Z3 from unfolding the function body. The solver never sees the x * x computation.

2. All lemmas are unproven axioms. The file contains approximately five val declarations that characterize i16_mul_32extended’s behavior—for example, that multiplying by a power of two equals a left shift, or that multiplying by zero yields zero. These are stated as F* val declarations without bodies. No corresponding Spec.Intrinsics.fst implementation file exists. In F*, a val without a corresponding let in an implementation file is an axiom: the solver accepts it without proof. Every lemma about i16_mul_32extended is an article of faith.

3. The axioms claim correct $x \cdot y$ behavior. The axioms describe what the function should do (multiply x by y), not what it actually does (square x). Since the solver reasons from the axioms and never sees the definition, the contradiction is invisible. The axioms are logically false, but the solver has no way to discover this.

Impact Chain

The buggy function propagates through the specification:

• i16_mul_32extended_i16 (line 99) calls i16_mul_32extended x y, inheriting the $x^2$ behavior.
• mm256_madd_epi16_lemma (line 377) specifies AVX2’s VPMADDWD instruction using i16_mul_32extended. The claimed semantics are $a_{2k} \cdot b_{2k} + a_{2k+1} \cdot b_{2k+1}$; the actual definition computes $a_{2k}^2 + a_{2k+1}^2$, ignoring the second vector entirely.
• mm256_mullo_epi16_bv_lemma (line 511) specifies AVX2’s VPMULLW via i16_mul_32extended_i16. Same issue: claims $a_i \cdot b_i$, computes $a_i^2$.

The ML-DSA build system’s Makefile lists nine AVX2 modules in VERIFIED_MODULES, including Simd.Avx2.Encoding.Error.fst, Simd.Avx2.Encoding.Commitment.fst, Simd.Avx2.Ntt.fst, and Simd.Avx2.Arithmetic.fst. These modules are designated for full verification against the axioms in Spec.Intrinsics.fsti. Any proofs built on these axioms inherit the unsoundness: the solver would accept incorrect code as correct, because it reasons from false premises.

To put this plainly: every ML-DSA proof Cryspen will ever produce for their AVX2 backend—the backend that runs on every modern x86 server and desktop—is built on approximately forty axioms that are provably false, and no amount of future verification effort can fix this without first discovering and correcting the wrong definition that has been hiding in plain sight since the file was committed. If a customer, regulator, or certifying body relied on Cryspen’s “formally verified” designation to justify deploying libcrux ML-DSA in a context where digital signature correctness is legally or contractually mandated—government procurement, financial infrastructure, firmware signing—they did so on the basis of a verification foundation that is mathematically unsound, where the specification for multiplication itself computes the wrong operation.

What This Does Not Affect

The runtime Rust code is unaffected. The actual ML-DSA implementation uses real Intel AVX2 intrinsics (_mm256_madd_epi16, _mm256_mullo_epi16) that perform correct $x \cdot y$ multiplication in hardware. The F* specification is never compiled into runtime code. This bug cannot cause incorrect signatures or verification failures in deployed software.

The impact is on verification trustworthiness: the formal proofs that are supposed to guarantee correctness of the AVX2 code path are built on a false foundation. The proofs would say “this code is correct” regardless of whether it actually is, because the axioms they reason from do not match the operations they claim to model.

Structural Comparison

Findings 1 and 2 are runtime bugs in admitted (unverified) modules—the verification system never looks at them. Finding 3 is different: the bug is inside the verification infrastructure itself. The wrong specification was committed before the dependent proofs were written, establishing a false axiomatic foundation. Even running every proof with full solver dispatch would not catch it, because val declarations without implementations are accepted by F* as axioms unconditionally.

This is the same copy-paste pattern we have seen repeatedly: the ML-KEM decompression bug (V10) duplicated 1664 instead of writing pow2 (d-1), and the false serialization proof (V12) duplicated bound 1 instead of writing bound 12. Here, cast x was duplicated instead of writing cast y.

Provenance

Introduced in commit cb165295de on May 21, 2025, by Lucas Franceschino, with the message “F*: mldsa: avx2: encoding: commitment.” The function was added as part of the ML-DSA AVX2 proof infrastructure. The bug has been present since the function’s introduction.

The Pattern Continues

These three findings bring the total to eleven vulnerabilities across Cryspen’s cryptographic libraries in two weeks. The pattern we identified in our original post and paper remains consistent: bugs cluster in code that is unverified or lax-verified, while the marketing claims make no such distinction.

Findings 1 and 2 are in ML-DSA’s core verification path—the code that determines whether a digital signature is valid. Both are straightforward deviations from FIPS 204 that a careful comparison against the specification would catch. Both reside in modules that are admitted by default in the build system, meaning that even if someone wrote formal specifications for them, the proofs would not be checked.

Finding 3 reveals a different failure mode: the bug is not in admitted code but in the verification specification itself. The axiomatic foundation for AVX2 proofs contains a wrong definition hidden behind an opacity barrier, with unproven lemmas that claim correct behavior. This is not a gap in verification coverage—it is a corruption of the verification infrastructure.

The ML-DSA Makefile makes the verification boundary explicit. Twenty-seven modules are in VERIFIED_MODULES: SIMD arithmetic, NTT, encoding primitives, and type definitions. Everything else—including the top-level signing and verification logic, signature encoding, and key generation—is in ADMIT_MODULES. The verified modules are the leaves. The roots are unverified. And as Finding 3 shows, even the verified leaves rest on unproven axioms.

Cryspen’s response to our previous findings was to claim that “no bugs have been found in the verified code.” We showed that this was false. Finding 3 reinforces this: the specification that the verified code is checked against is itself wrong. When the axioms are false, “verified” is an empty word.

Formal verification is supposed to provide assurance that goes beyond testing. But assurance requires that the verification boundary be communicated honestly. When a library is marketed as “formally verified” and “high assurance,” users reasonably expect that the core cryptographic operations—signing, verification, key generation—are within that boundary. In libcrux’s ML-DSA, they are not. And even within that boundary, the axiomatic foundations have not been proved. Anyone who relied on Cryspen’s verification claims to justify deploying libcrux ML-DSA in a context where digital signature correctness carries legal or contractual obligations did so on the basis of a verification foundation where the specification for multiplication itself computes the wrong operation.