Quantum Cryptography and Autoformalization in Lean

We formalized an end-to-end security proof for quantum cryptography (the BB84 protocol) in the Lean proof assistant, down to the mathematical axioms. The proof covers composable finite-key security of entanglement-based BB84 against coherent attacks. To our knowledge, it is the first machine-checked proof of its kind.

The proof was enabled by LLM-based autoformalization. Getting proofs to compile is the easy part. Knowing whether they prove what we meant takes domain experts who check the theorem statement and every definition it depends on. The protocol is written in a language that allows only local operations and classical communication, the steps two separate labs can actually perform, which keeps the formal statement faithful to the physics. With the proof complete, we used the same pipeline as a discovery machine and reduced the finite-size penalty on the key rate, again checked by Lean.

Led by Maor Ben-Shahar, with Jonathan Morag, Dirk Englund and Kfir Sulimany (senior author). The work will be presented at QCrypt 2026.

• Paper: Quantum Cryptography and Autoformalization in Lean, arXiv:2610.17286
• Lean library: QCryptLean
• Agentic framework: loopy
• Dependency-graph tools: lean-graph-tools