In our connected world, people rely on cryptographic libraries to keep messages, transactions, and identities safe from prying eyes and to ensure that the messages can be trusted. When a library carries the label of formal verification, many assume that a computer has exhaustively confirmed every detail of its behavior. A close examination of several widely adopted libraries shows that this assumption often rests on a less complete foundation than the label suggests.[1]
Formal verification applies precise logical rules and automated tools to demonstrate that software follows its intended rules under every possible set of inputs. In cryptographic libraries, it serves to establish that operations produce the correct results, that no secret values leak through timing differences or memory errors, and that the code behaves consistently even when faced with unexpected data. The goal is to replace reliance on testing alone with mathematical-style guarantees that certain classes of errors cannot occur. These guarantees matter because cryptographic code handles the most sensitive data in modern systems, and even small deviations can open the door to attackers.
The process begins with a detailed specification written in a language built for exact reasoning. Developers then write an efficient implementation, often in a language such as Rust. Specialized extraction tools translate the implementation into a form that a proof assistant can examine. Inside the proof assistant, solvers check whether the code matches the specification and satisfies additional required properties. Once proofs are complete for the targeted parts, the verified source code is compiled by ordinary compilers for real machines. At that point, the guarantees no longer apply directly to the compiler output or to any hardware-specific instructions that may replace parts of the code for speed.
This sequence naturally creates a dividing line. On one side of the line sits the code for which machine-checked proof exists. On the other side lies everything that must be accepted without such proof: the compiler itself, the operating system, the specific instructions provided by different processor designs, and the additional code that connects the verified core to the rest of an application. The line is unavoidable because proving an entire computing stack from silicon upward would be impractical for most projects. When the location and nature of this dividing line remain unclear to users and developers, the result is a mismatch between what is claimed and what has been established.
The paper “Verification Theatre: False Assurance in Formally Verified Cryptographic Libraries” by Nadim Kobeissi identifies this mismatch as verification theatre. It arises when a project presents machine-checked proofs for selected components while using language that implies broader coverage, without disclosing which parts remain unexamined or which proofs were accepted without full checking. Practice does not require deliberate deception. It can occur through incomplete documentation, building configurations that skip verification steps by default, or marketing statements that do not reflect the actual scope of the proofs.
Kobeissi applied a systematic review to libraries developed by CE Labs, including libcrux and hpke-rs. These libraries supply cryptographic functions for projects at Google, within Signal, and in OpenMLS. The review uncovered thirteen distinct issues that had passed through the verification process. Nine of the issues appeared in code that sat outside the verified portion. Four appeared inside the specifications and proofs themselves.
The issues outside the verified portion included cases where code produced different results on different types of processors because byte ordering was handled inconsistently across implementations. One such inconsistency affected an incremental interface used in Signal’s post-quantum messaging features, leading to decryption failures for users across several operating systems until a fix was applied. Other issues involved the absence of checks required by published standards for key exchange operations, sequence counters that wrapped around without detection and allowed reuse of values that should remain unique, code that terminated an entire process instead of reporting an error when decryption failed, extra processing steps during key generation that reduced the effective randomness available, and safety checks inside signature verification routines that were either set too loosely to catch problems or that examined the wrong data and therefore missed violations.
The four issues found inside the verified specifications and proof were more fundamental. One specification used an incorrect constant when describing how to recover values from compressed data, a copy-paste error that meant proof established correctness relative to the wrong mathematical rule. Another specification omitted a required transformation step when describing encryption, so that later proofs related implementations to an incomplete description. A third case contained a proof statement claiming that values spanning twelve bits were bound by a range that holds only single-bit values, a claim that could only be accepted because the module containing it was not subjected to full checking. The fourth case defined a multiplication operation within the axioms used for optimized processor-specific code, in a way that computed a number multiplied by itself rather than by a second number, rendering any proofs built on those axioms unreliable for the intended operation.
These problems fell into five recurring patterns. Some stemmed from platform-specific instructions whose actual behavior on certain processors did not match the abstract model used in proofs. Others arose in the higher-level logic that calls the verified primitives, where required checks or error handling were omitted. Another pattern involved specifications that were internally consistent yet failed to capture constraints needed in real deployments, such as rules for unique signatures used by major cryptocurrency systems. A fourth pattern appeared in the connecting code that assembles verified building blocks into complete functions, where simple mistakes in ordering or variable selection introduced defects. The fifth and most concerning pattern involved errors within the specifications or proofs, often surviving because building systems accepted entire modules without running the solvers, or because special checking modes silently approved unproven statements.
The findings carry weight because they affect libraries already in active use. The processor-related inconsistency, for example, produced concrete failures in a widely deployed messaging system. Signature verification problems could allow one implementation to accept signatures that another conforming implementation would reject, creating inconsistencies in systems that rely on consistent validation across participants. Nonce reuse and missing validation checks represent classic avenues for recovering plaintext or forging messages if an attacker can trigger the relevant conditions. Because the libraries support post-quantum algorithms being integrated into production systems, weaknesses at this stage can affect the security posture of organizations adopting them.
Kobeissi also compared the practices observed in the CE Labs libraries with those used in AWS’s verified cryptographic work. Both efforts encounter the same categories of potential gaps. The AWS projects, however, explicitly state that their scope covers portions of their libraries rather than claiming comprehensive verification. They automatically perform proof checking on every code change through continuous integration pipelines and maintain machine-readable records of what has been verified on which platforms. These differences illustrate that the patterns identified are not inevitable but depend on choices about documentation, automation, and the handling of proof obligations.
To help others identify similar situations, the paper outlines a practical four-step review process that requires only standard text-editing and command-line tools. The first step maps the dividing line by locating annotations that exclude code from extraction and by examining build scripts for settings that admit modules without full checking. The second compares the formal specifications directly against published standards, paying particular attention to constants, required transformation steps, and claimed bounds on values. The third confirms that proof obligations are sent to solvers rather than bypassed through default admission or lax-mode tactics that accept claims without examination. The fourth step checks whether public documentation and marketing statements align with the building system's actual configuration.
The work points toward several concrete next steps for the broader community. Projects that publish verified libraries can adopt machine-readable manifests that list exactly which modules, properties, and target platforms have completed proofs. Continuous integration systems can be configured to run full verification on every change, with slower proofs flagged rather than skipped. Proof tactics can be written to explicitly fail in lax modes rather than silently approve goals. Documentation can state limitations in the same prominent way as capabilities. When these habits become standard, the gap between verification claims and verification practice narrows, and downstream users receive a clearer picture of the assurances they are receiving.
Formal verification remains one of the strongest available methods for increasing confidence in cryptographic code. Its value, however, depends on consistent execution of the proofs and transparent description of their reach. By making the dividing line visible and ensuring that claims match the work performed, developers and users alike can obtain more reliable protection for the systems that safeguard sensitive information every day.
This article is shared at no charge for educational and informational purposes only.
Red Sky Alliance is a Cyber Threat Analysis and Intelligence Service organization. We provide indicators of compromise information (CTI) via a notification/Tier I analysis service (RedXray) or an analysis service (CTAC). For questions, comments, or assistance, please contact the office directly at 1-844-492-7225 or feedback@redskyalliance.com
- Reporting: https://www.redskyalliance.org/
- Website: https://www.redskyalliance.com/
- LinkedIn: https://www.linkedin.com/company/64265941
Weekly Cyber Intelligence Briefings:
REDSHORTS - Weekly Cyber Intelligence Briefings
https://attendee.gotowebinar.com/register/7855487668891299929
[1] https://six3ro.substack.com/p/when-computer-proven-security-leaves
Comments