tl;dr: A hands-on tutorial introducing formal verification in Lean 4 for cryptography engineers, using the One-Time Pad as a worked example. It walks through defining bitstrings and XOR over ℤ₂, proving XOR's commutativity, associativity, identity, and self-inverse properties using tactics like `Vector.ext`, `simp`, and `intro`, then defines a Shannon cipher as a Lean `structure` and proves OTP satisfies its correctness property. Based on Boneh & Shoup's textbook, it's aimed at beginners and serves as a stepping stone to more advanced formalizations like VCV-io.