- Author
- Elena, Cryptography Engineer at HashCloak
- Published
- 15 July 2026
- Kind
- Company blog tutorial with code-along Lean examples
- Original
- hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)
- Subject
- Checkable specs for coding agents
- Themes
- Checking the work, Getting good
What it is
Elena, a cryptography engineer at HashCloak, wrote this tutorial. It ports definitions and proofs from a graduate cryptography textbook into Lean. The author says it is not a guide to Lean best practice.
What it says
- Lean lets people write proofs as code and have the compiler check them.
- The tutorial defines bit strings as vectors over integers mod two, and XOR as addition.
- It proves XOR is commutative and associative, and has an identity and self-inverse.
- A Shannon cipher is modeled as a structure with encryption, decryption and a correctness proof.
- The one-time pad's correctness follows from the XOR lemmas, by the textbook's own proof.
- Proofs cover a model of the code, so gaps can remain between code and theorem.
What evidence it gives
The tutorial gives full Lean code for each step. It ends with a 57-line final listing. It shows what Lean reports at each proof step. It does not run benchmarks. The closing remarks on blockchain verification cite other writing without testing it.
Interests and limits
The post is a tutorial, not a study. It notes a compiled proof is correct only assuming trust in the Lean compiler. Only the correctness of the one-time pad is proved, not its security. The author says security is left for a part two. The post says the proof style is lengthy and not best practice.