Cryspen is a company that markets itself as providing “services and software for high assurance software in order to establish trust into your critical systems.” Their flagship product, libcrux, is billed as a cryptographic library that “has been formally verified” and offers “the highest level of assurance”, translating into that it is safe to use and free of bugs.

In the past two days, we at Symbolic Software have submitted four pull requests to Cryspen’s repositories addressing security vulnerabilities and implementation defects. These findings follow an incident from late 2025 in which libcrux produced silently incorrect cryptographic outputs on certain platforms: a bug that Cryspen addressed quietly, without any public disclosure, and which only received a security advisory because third parties took it upon themselves to file one.

This pattern of events invites reflection on what “high assurance cryptography” actually means, and whether the formal verification community has developed a habit of overpromising and underdelivering.

The Original Incident: Platform-Dependent Cryptographic Failures

In November 2025, Filippo Valsorda reported that libcrux-ml-dsa v0.0.3 produced different outputs depending on the execution environment. The same seed input generated different public keys and signatures on Alpine Linux with Ampere Altra ARM64 hardware compared to macOS on Apple Silicon. This was not an edge case in error handling or a performance regression—this was the core cryptographic functionality producing incorrect results.

The bug resided in an unverified fallback implementation for the vxarq_u64 intrinsic. On platforms lacking native SHA-3 instruction support, the fallback passed incorrect arguments, corrupting SHA-3 digests and causing downstream cryptographic operations to fail silently. Any system relying on this code for ML-DSA signatures or ML-KEM key exchange would have experienced authentication failures or key agreement mismatches, depending on which platform generated the cryptographic material.

Cryspen fixed the bug. What they did not do was issue any public disclosure, security advisory, or acknowledgment that their “formally verified” library had shipped with a defect that caused silent cryptographic failures in production environments.

The Burial

The only security advisory that exists for this vulnerability was not initiated by Cryspen. It was filed by Joe Birr-Pixton (ctz) in the RustSec advisory database—a third-party effort to document the vulnerability for the Rust ecosystem. The advisory was merged on December 4, 2025, after Cryspen provided “refined wording” that emphasized the bug was in “libcrux-intrinsics” rather than the downstream packages.

This framing is technically accurate and practically misleading. The intrinsics crate is an internal dependency of libcrux-ml-kem and libcrux-ml-dsa. Users of those libraries experienced corrupted cryptographic operations. The distinction between “the intrinsic layer had a bug” and “the cryptographic library produced wrong outputs” matters to Cryspen’s marketing narrative but not to anyone whose systems were affected.

There was no blog post. No security bulletin. No announcement on any Cryspen communication channel. No email to known users of the library. The RustSec advisory—which most developers will never see unless they actively run cargo audit—represents the entirety of Cryspen’s disclosure posture for a bug that caused their formally verified cryptographic library to produce incorrect outputs.

Compare this to how other cryptographic library maintainers handle similar situations. When the Kyber reference implementation contained a variable timing vulnerability in late 2023, it was the subject of extensive public discussion, a dedicated tracking website (KyberSlash), and advisories from affected downstream implementations. When we discovered the same vulnerability in our own Kyber-K2SO implementation, we issued a public security announcement within 24 hours; we were among the first to do so.

Cryspen’s approach was to fix the bug, avoid any public acknowledgment, and wait for someone else to file an advisory in an obscure database.

Four New Findings

Between February 3 and February 4, 2026, we identified four additional issues in Cryspen’s cryptographic libraries. These range from specification non-compliance to entropy reduction to potential nonce reuse.

1. Missing X25519 All-Zero Validation (hpke-rs)

Pull request #117 addresses a missing validation required by RFC 9180, the HPKE specification. Section 7.1.4 of the RFC mandates that implementations “MUST check whether the Diffie-Hellman shared secret is the all-zero value and abort if so.”

The X25519 function, when given certain low-order points as input (such as the identity element or points of small order), produces an all-zero output. If an attacker can supply a malicious public key, they can force the shared secret to be zero, making the subsequent key derivation deterministic and predictable.

This vulnerability concerns an explicit requirement in the specification that the implementation claimed to follow. The fix is trivial: a single comparison after the DH computation. Its absence indicates that either the specification was not read carefully or the requirement was deprioritized.

2. Nonce Reuse via Sequence Number Overflow (hpke-rs)

Pull request #118 addresses a flaw in how HPKE sequence numbers are managed. The library stores the sequence number as a u32, which has a maximum value of approximately 4.3 billion. RFC 9180 specifies that the sequence number must be checked against 2^96 - 1 for standard 12-byte nonces.

The overflow check in the original code compared a u32 against a value that a u32 can never reach. In debug builds, Rust’s overflow checking would cause a panic when the counter wrapped. In release builds—the builds that actually run in production—the counter would silently wrap to zero, reusing nonces.

Nonce reuse in authenticated encryption is catastrophic. For AES-GCM, it enables recovery of the authentication key and XOR of plaintexts. For ChaCha20-Poly1305, it directly enables plaintext recovery through XOR attacks. Any application encrypting more than 4.3 billion messages with the same HPKE context would be vulnerable.

The fix is one line: replace + with checked_add(). The fact that this was not already the implementation suggests that the security implications of integer overflow in cryptographic contexts were not adequately considered.

3. ECDSA Signature Malleability (libcrux)

Pull request #1315 addresses signature malleability in the ECDSA P-256 implementation. For any valid ECDSA signature (r, s), there exists an alternative valid signature (r, n - s), where n is the curve order. Without low-S normalization—constraining s to be at most n/2—signatures are malleable: an attacker can produce alternative valid signatures without knowing the private key.

This matters in practice. Bitcoin’s BIP 62 and BIP 146 mandate low-S normalization because signature malleability can alter transaction identifiers, potentially enabling theft and breaking transaction chains. More generally, any system that uses signatures for deduplication, audit trails, or caching can be confused by malleable signatures.

The libcrux implementation validates that r and s are nonzero but does not compare s against n/2 or apply normalization. This is a well-known requirement that has been standard practice in ECDSA implementations for over a decade.

4. Ed25519 Double Clamping (libcrux)

Pull request #1316 addresses an unnecessary entropy reduction in Ed25519 key generation. The generate_key_pair function was applying scalar clamping operations to the raw seed before hashing:

1
2
3

sk[0] &= 248u8;
sk[31] &= 127u8;
sk[31] |= 64u8;

According to RFC 8032, clamping should occur after SHA-512 hashing of the seed, not before. Applying these operations to the raw seed removes 5 bits of entropy (3 from the first byte, 2 from the last), reducing the effective key space from 256 bits to 251 bits.

While 251 bits remains computationally secure against brute force, there is no benefit to this reduction. The SHA-512 hash produces a uniformly distributed output regardless of input patterns; clamping the input serves no cryptographic purpose. It only reduces entropy without providing any compensating advantage.

This is not a subtle issue. The Ed25519 specification is explicit about when clamping occurs. Implementing it incorrectly suggests either that the specification was not consulted or that its requirements were misunderstood.

What Does This Tell Us About “High Assurance Cryptography”?

The formal verification community has developed a vocabulary for marketing that systematically overstates what verification actually accomplishes. When Cryspen claims their library is “formally verified” and “free of bugs,” they are making statements that their own bug history contradicts.

The November 2025 incident is instructive. The bug was in an ARM SIMD intrinsic fallback—precisely the kind of low-level, platform-specific code that formal verification tools cannot reason about. Formal verification in practice means verifying an abstract model, then trusting that the compiler, the intrinsics, the runtime, and the hardware all faithfully implement that model.

This is not verification in the sense that users understand the term. It is verification of a Rust model, plus hope that LLVM generates correct code, plus hope that the ARM instruction set behaves as documented, plus hope that every CPU implementation thereof is free of errata, plus hope that the operating system, memory allocator, and runtime environment introduce no observable differences.

The honest description would be: “We have verified portions of our Rust code against certain properties using the hax toolchain. The actual security of deployed systems depends on your compiler version, target architecture, CPU microcode, operating system, and numerous other components we cannot verify.” But that does not sell. It does not win grants. It does not attract customers.

Instead, we get “formally verified” as a marketing term, a way to claim superiority over libraries that rely on extensive testing, fuzzing, cross-platform validation, and code review—the engineering practices that might have caught the platform-dependent output bug before it shipped.

The four new findings reinforce this pattern. None of them involve subtle interactions between verified and unverified code. They are straightforward implementation defects:

• A specification requirement that was ignored (X25519 zero check).
• An integer type that was too small for its purpose (sequence number overflow).
• A normalization step that was omitted (ECDSA low-S).
• A clamping operation that was applied at the wrong point (Ed25519 double clamping).

These are not the kinds of bugs that formal verification is designed to catch. They are the kinds of bugs that careful code review, comprehensive testing, and attention to specifications would catch. They suggest that the development process prioritized the verifiable core over the engineering fundamentals that surround it.

The Verification Theater Problem

There is a pattern in the formal methods community that might be called “verification theater”: the deployment of formal methods in ways that create the appearance of rigor without delivering its substance.

A cryptographic library that is “formally verified” but ships with platform-dependent incorrect outputs has not achieved high assurance. It has achieved a verified core surrounded by an unverified periphery that can fail in ways that make the verification meaningless.

A company that fixes critical bugs without disclosure has not demonstrated trustworthiness. It has demonstrated that marketing concerns outweigh transparency obligations.

A codebase that lacks basic specification compliance—checking for all-zero DH outputs, preventing integer overflow, normalizing signatures—has not been developed with the care that “highest level of assurance” implies.

The formal verification community needs to develop more honest communication practices. Verification is valuable. It catches certain classes of bugs that testing cannot. But it is not a substitute for engineering discipline, and claiming otherwise undermines both the credibility of formal methods and the security of users who trust those claims.

When a formally verified cryptographic library produces platform-dependent incorrect outputs for its core primitive, and that library’s maintainers bury the disclosure while continuing to market the library as “free of bugs,” we must ask: free of which bugs, verified against which properties, and trustworthy to whom?

The answers, in Cryspen’s case, appear to be: not the bugs that matter, not the properties users care about, and not to anyone paying close attention.