La verificación formal permite demostrar la corrección de enunciados matemáticos escribiendo la prueba en código para que un programa la valide mecánicamente. Entre las herramientas disponibles se encuentran Rocq (antes Coq), Isabelle y Lean, esta última creada en 2013 por Leonardo de Moura en Microsoft Research. Lean combina un lenguaje de programación funcional puro con un asistente de demostración: los teoremas se redactan junto con sus demostraciones y, si el compilador las acepta, se consideran correctas (asumiendo confianza en el compilador). Además, facilita dividir las pruebas en subpruebas, colaborar en ellas y completarlas automáticamente.
Este tutorial, firmado por Elena, ingeniera de criptografía en HashCloak, está dirigido a profesionales de la criptografía que se acercan por primera vez a la verificación formal o desean repasar sus fundamentos. A lo largo de cuatro partes tras un breve "Hola mundo", los lectores codificarán en Lean 4 la verificación del protocolo One-Time Pad (OTP), un cifrado popularizado por Claude Shannon y descrito previamente por Frank Miller y Gilbert Vernam.
El material toma como referencia principal el libro "A Graduate Course in Applied Cryptography" de Dan Boneh y Victor Shoup, del que se移植an al asistente las definiciones y demostraciones. En esta primera parte se sientan las bases: se define el tipo BitString como vector de elementos de ZMod 2, se implementa la función XOR y se demuestran sus propiedades fundamentales (conmutatividad, asociatividad, elemento identidad y autoinversión). Las partes siguientes abordarán la definición de un cifrado de Shannon con sus funciones de cifrado, descifrado y propiedad de corrección, para finalmente demostrar que el OTP, donde cifrar y descifrar se reducen a XOR, cumple esa definición.