Tutorial: Introduction to Formal Verification with Lean (Part 1) - HashCloak
hashcloak.com
A tutorial Formal Verification using Lean for cryptographic engineers. Implement and prove correctness of the One-Time pad following a cryptography book.