FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq

arXiv:2610.30645 · quant-ph, cs.CR, cs.LO · Submitted 2026-10-22 · Read on arXiv

quant-ph, cs.CR, cs.LO

Submitted: 2026-10-22

Updated: 2026-10-22

Terminology

• Formal Verification — 1× in this paper · explained in 2 episodes
• Verification — 1× in this paper · explained in 2 episodes

Related papers

• Reconquering Bell sampling on qudits: stabilizer learning and testing, quantum pseudorandomness bounds, and more
• Encrypted clones can leak: Classification of informative subsets in Quantum Encrypted Cloning
• Polynomial-time classical and quantum simulation of quantum impurity models
• Incoherent Imaging with Spatially Structured Quantum Probes
• A quasiparticle-protected superconducting qubit
• Theory of quantum-enhanced interferometry with general Markovian light sources