The Signal
Rocq and Lean Teams Formalize BB84 Security in Separate Proofs
A Rocq paper submitted October 22 reports a machine-checked proof of composable, finite-key security for BB84, after an earlier Lean paper described an end-to-end security theorem for a specific BB84 formulation. The papers use different pr
Quantum.world Team · Written with AI · fact-checked ·
Two formal developments for BB84
A paper submitted to arXiv on October 22 presents FVQKD, a Rocq library for machine-checking quantum key distribution security proofs. Its authors describe the library’s first result as an end-to-end machine-checked proof of composable, finite-key security for BB84. A separate paper, submitted October 12, describes an end-to-end security theorem formalized in Lean. The papers use different proof assistants and approaches, and the Lean paper’s abstract does not claim that its result was first.
The earlier Lean paper covers composable security of the entanglement-based qubit BB84 protocol against coherent attacks, using the postselection technique and accounting for finite block size. FVQKD describes a complete proof of composable, finite-key security for BB84, and reconstructs the mathematical infrastructure used in its development. The two abstracts therefore describe related but distinct formal results, without making matching priority claims.
What FVQKD checks
FVQKD reconstructs the mathematical machinery needed for its BB84 proof, including the smooth-entropy framework, the entropic uncertainty relation and the Quantum Leftover Hash Lemma. Its authors say they connect the information-theoretic security bound to a formal semantics of protocol execution, so the protocol’s modeled steps are part of the checked development.
“Its first result is a complete, end-to-end machine-checked proof of composable, finite-key security for BB84.”
Ruixuan Deng, Zhengfeng Ji, Jiayu Zhang and Li Zhou, authors of FVQKD
The paper reports that formalization exposed necessary side conditions left unstated in a published argument, including one that revealed a missing proof branch. This is a finding about the completeness of a mathematical derivation, not evidence that BB84 is broken or that a deployed QKD system has been compromised. The authors say their proof contains no admitted steps and relies on the Rocq kernel and standard foundational axioms.
How the earlier Lean work differs
The October 12 paper formalizes an entanglement-based qubit version of BB84 and uses postselection to extend its security analysis to coherent attacks. Its Lean-defined protocol language enforces local operations and classical communication. The authors also report using the same pipeline as a discovery method, reducing the finite-size penalty on the key rate. The abstract does not characterize that result as a tighter conditional-entropy-variance bound.
FVQKD, by contrast, is built in Rocq on MathComp, MathComp-Analysis and CoqQ. Its authors present the proof infrastructure as reusable for other QKD variants and quantum-cryptography applications. The papers are separate formal developments, rather than interchangeable implementations of one proof. The Rocq abstract calls its result the first end-to-end formal verification of a QKD security proof; the Lean abstract describes an end-to-end theorem but does not make a first-priority claim.
A proof of a model, not a hardware audit
Machine checking can catch mistakes in formal reasoning, but it does not by itself establish that a real-world transmitter, detector or communication link behaves like the mathematical protocol. FVQKD concerns a formal security proof, not a test of deployed QKD equipment. Its authors describe the library as infrastructure intended for reuse in further work on related protocols.
The papers were submitted to arXiv on October 12 and October 22, 2026, respectively. The Lean work formalizes a security theorem for entanglement-based qubit BB84 against coherent attacks; the Rocq work reports a complete proof of composable, finite-key BB84 security and a missing branch in a published argument. Their abstracts describe different contributions, and only the Rocq paper makes an explicit claim to be the first end-to-end formal verification of a QKD security proof.