The Broken Promises of 'High-Assurance' Cryptography

The cryptographic community faces uncomfortable questions about the meaning of "high-assurance" following a series of security vulnerabilities discovered in Cryspen's formally verified libraries. Despite marketing claims of offering "the highest level of assurance," multiple implementation defects have been found in libcrux and related projects, accompanied by concerning disclosure practices that undermine trust in verification claims.

The Silence of Verified Failures

In November 2025, libcrux-ml-dsa exhibited platform-dependent cryptographic failures where identical seeds produced different public keys and signatures across ARM64 and Apple Silicon architectures. The root cause was an unverified intrinsic fallback implementation for SHA-3 instructions. Crucially, Cryspen fixed this silent failure without public disclosure or security advisory. The only existing advisory was filed by third parties in the RustSec database—an action Cryspen later reframed as concerning only an "internal dependency" rather than acknowledging core cryptographic functionality failure.

This pattern continued when Symbolic Software recently submitted four critical pull requests addressing new vulnerabilities:

1. HPKE Specification Violation: Missing validation for all-zero Diffie-Hellman outputs (PR #117), violating RFC 9180 and enabling predictable key derivation

2. Nonce Reuse via Integer Overflow: Sequence number counter overflow in HPKE (PR #118) causing catastrophic nonce reuse in production builds

3. ECDSA Malleability: Absence of low-S normalization (PR #1315) enabling signature manipulation attacks

4. Ed25519 Entropy Reduction: Incorrect clamping during key generation (PR #1316) reducing effective key space by 5 bits

These aren't edge-case failures but fundamental implementation defects contradicting specification requirements—the very bugs formal verification claims to prevent.

The Verification Theater

Formal verification's marketing vocabulary systematically overstates capabilities. When Cryspen claims their library is "free of bugs," they implicitly define "bugs" only as deviations from their abstract Rust model. Real-world deployment involves unverified components: compilers, CPU microcode, operating systems, and intrinsic implementations. The November 2025 failure occurred precisely where verification's reach ends—in platform-specific intrinsics.

This creates verification theater: rigorous mathematical proofs applied to an idealized model while ignoring the unverified periphery where failures manifest. The four new findings further demonstrate how specification compliance and cryptographic fundamentals were overlooked. Missing zero-checks, integer overflow handling, and normalization requirements represent engineering oversights that code review and testing should catch—regardless of formal methods.

Toward Honest Assurance

Formal verification provides real value against specific bug classes, but marketing it as comprehensive "high assurance" creates dangerous illusions. Cryptographic libraries claiming verification must:

1. Explicitly document verification boundaries and residual risks
2. Maintain disclosure practices commensurate with claimed trust levels
3. Complement verification with rigorous specification compliance testing

The community must reject verification theater—where mathematical proofs become marketing tools while engineering fundamentals languish. When libraries produce platform-dependent incorrect outputs and maintainers avoid disclosure while claiming bug-free status, we must ask: assurance for whom, against what threats, and verified by which criteria? Until these questions receive honest answers, "high-assurance" cryptography remains an unfulfilled promise.