Welcome to Formal Methods

Formal Cryptography in Lean

• One-time Pad in Lean collects notes on using the Lean proof assistant to formally state and prove some basic theorems in cryptography.

• lean4crypto is a repository, available at https://github.com/formalverification/lean4crypto, containing Lean programs for formalizing basic cryptography, as described in the notes collected in the One-time Pad in Lean section.

• lean4crypto documentation is available at https://formalverification.github.io/lean4crypto/OTP/Basic.html.