Introduction to Formal Verification with Lean (Part 1)

Author: Elena, Cryptography Engineer
Date: July 15, 2026
Source: HashCloak Insights

---

What is Formal Verification?

Formal Verification is a rigorous method used to prove the correctness of mathematical statements.

While traditional mathematics relies on pen-and-paper proofs, formal verification allows us to translate those proofs into code. This code is then processed by a machine to ensure that the logic is flawless, removing the risk of human error in the proof process.

Tooling Landscape

Several tools exist for this purpose, including:

• Rocq (previously known as Coq)
• Isabelle
• Lean $\leftarrow$ The focus of this tutorial

Tutorial Objectives

This series is designed for cryptographic engineers—whether you are a complete novice to formal verification or simply looking for a refresher. We will walk through the fundamentals of Lean and apply them to verify the One-Time Pad (OTP) protocol, a system pioneered by Frank Miller and Gilbert Vernam and later popularized by Claude Shannon.

Our primary mathematical reference for definitions and proofs is “A Graduate Course in Applied Cryptography” by Dan Boneh and Victor Shoup. By the end, you should be comfortable enough to explore advanced formalized proofs, such as those found at VCV-io.

Disclaimer: This guide is an introductory exploration for crypto-enthusiasts; it is not intended to be a definitive guide on Lean best practices.

---

Understanding the Lean Proof Assistant

Developed in 2013 by Leonardo de Moura at Microsoft Research, Lean is a powerful tool that allows mathematicians to formalize axioms, lemmas, and theorems.

Key Characteristics of Lean

Learning Path

If you want to dive deeper, here are some recommended resources:

• The Hitchhiker’s Guide to Logical Verification (Beginner exercises)
• Functional Programming in Lean (Introductory book)
• The Natural Number Game (Interactive browser-based proving)

Note: While these resources are excellent, this tutorial specifically bridges the gap between Lean and cryptography, as VCV-io's materials are often too advanced for beginners.

---

Getting Started: "Hello World"

Environment Setup

You can install Lean locally or use the online editor. The interface is split into two main sections:

1. Left Pane: Where you write your Lean code.
2. InfoView (Right Pane): Where Lean provides feedback, errors, and evaluation results.

To test your setup, try running this command: #eval 1 + 1 You should see the result 2 appear in the InfoView.

Basic Examples

For a classic "Hello World," you can use these snippets:

-- Simple string evaluation
#eval "Hello World!"

-- Using a conditional and string concatenation
#eval String.append "Hello " (if 1 < 2 then "Lean!" else "World!")

Essential Lean Syntax

• Math Conventions: Lean follows standard order of operations. For example, #eval 4 + 5 * 6 results in $4 + (5 \times 6) = 34$.
• Function Application: Lean does not use parentheses for arguments. You write f x instead of f(x).
• First-Class Functions: Functions are treated as values, similar to integers or strings.

---

The Path to Verifying the One-Time Pad

To use Lean effectively, we need absolute precision. We rely on the Boneh-Shoup text to ensure our mathematical definitions are airtight before translating them into code.

The Shannon Cipher

A Shannon Cipher is defined by three primary components:

1. An Encryption function.
2. A Decryption function.
3. A Correctness Property: The requirement that decrypting an encrypted message must return the original plaintext.

The One-Time Pad (OTP)

In the case of the OTP, both encryption and decryption are performed using the XOR (exclusive-OR) operation. To prove the OTP is a Shannon Cipher, we must first prove several properties of XOR:

• Commutativity: $a \oplus b = b \oplus a$
• Associativity: $(a \oplus b) \oplus c = a \oplus (b \oplus c)$
• Identity Element: $a \oplus 0 = a$
• Self-Inverse: $a \oplus a = 0$

Tutorial Roadmap

Coding Convention for this Tutorial:

• Line Numbers: Code with line numbers is essential for the final proof.
• No Line Numbers: This is scratchpad code for testing and can be deleted.
• Comments: New concepts are highlighted in comments at the start of each subsection.

---

Tutorial Part 1: Defining BitStrings and XOR

The One-Time Pad operates on keys ($K$), messages ($M$), and ciphertexts ($C$). All three are bit strings of a fixed length $L$.

Mathematically, this is represented as: $K := M := C := \{0,1\}^L$