Paper 2026/192

Verification Theatre: False Assurance in Formally Verified Cryptographic Libraries

Abstract

Every formally verified system embeds a verification boundary: the interface between code with machine-checked proofs and code that is trusted without them. We study what happens when this boundary is not communicated clearly. Through a case study of CE Labs's libcrux and hpke-rs cryptographic libraries, we present thirteen vulnerabilities that escaped formal verification. Nine reside in unverified code, including a cross-backend endianness bug that caused real decryption failures in Signal's post-quantum ratchet, a missing mandatory X25519 validation, nonce reuse via integer overflow, and two FIPS~204 specification violations in the ML-DSA verifier. Four reside in formally verified specification and proof code: in ML-KEM, a wrong decompression constant, a missing inverse NTT, and a false serialization proof; in ML-DSA, a wrong multiplication specification that renders axiomatized AVX2 proofs unsound. From these findings, we develop a taxonomy of five verification boundary failure types, a lightweight auditing methodology for detecting them, and a comparative analysis with AWS's verified libcrypto. The same failure types arise in both projects, but their management---through systematic documentation, proof execution in CI, and clear scope communication---varies significantly. We call the gap between verification claims and verification reality "verification theatre", and propose concrete practices for closing it.

Note: This update is a major rewrite of the paper bringing the total number of discussed bugs to thirteen, of which eleven are novel, and of which at least four occur within CE Labs's verification boundary. The paper also now includes many new sections, including a comparative study between libcrux and the verified components of Amazon's LibCrypto.