Core Idea
Lean 4 tutorial demonstrating formal verification of the One-Time Pad protocol — from defining BitString and XOR operations in dependent types to proving Shannon Cipher correctness with machine-checked proofs.
Why It Matters
Formal verification is entering mainstream engineering practice: Zcash, Ethereum (leanEthereum), and Nethermind are all using Lean to verify zkVMs, circuits, and smart contracts. Complements traditional testing (cf. “Ten ways a check passes while broken” anti-patterns) for security-critical systems.
Technical Details
- Dependent types: Vector (ZMod 2) L encodes bitstring length at the type level
- Curry-Howard isomorphism: proofs are programs verified by the type system
- XOR properties (commutativity, associativity, identity, self-inverse) → OTP correctness proof
- Resources: Natural Numbers Game, Functional Programming in Lean, Theorem Proving in Lean 4
Utility for Hermes
- Security-critical components (message bus auth, key management) could benefit from formal verification
- “Proofs as programs” mindset improves testing quality in CI/CD pipeline