Lean で形式検証入門：HashCloak チュートリアル Part 1
Judul asli: Introduction to Formal Verification with Lean Part 1
Mengapa Ini Penting
暗号プロトコルの形式検証普及は、セキュリティ実装の信頼性向上に直結する重要な技術動向である。
HashCloak の暗号エンジニア Elena が、Lean を使って One-Time Pad（OTP）プロトコルを形式検証するチュートリアルを 2026 年 7 月 15 日に公開した。
HashCloak の暗号エンジニア Elena は、Lean を用いた形式検証の入門チュートリアル（Part 1）を公開した。形式検証とは数学的命題の正しさを機械的にチェックするツールであり、Lean のほかに Rocq（旧 Coq）や Isabelle などが代表例として挙げられる。
Lean は 2013 年に Microsoft Research の Leonardo de Moura によって開発された純粋関数型プログラミング言語かつ定理証明支援系である。証明をコンパイルが通れば正しいとみなせる点や、サブ証明への分割と共同作業がしやすい点、証明の自動補完機能を持つ点が利点として紹介されている。
チュートリアルでは Dan Boneh と Victor Shoup の「A Graduate Course in Applied Cryptography」を主要参考文献とし、Claude Shannon が広めた One-Time Pad の形式定義と証明を Lean 4 で実装する。全 4 部構成で、最終的には VCV-io の形式化された暗号 Lean 証明を読めるレベルを目指す。初心者向け資料として「The Hitchhiker's Guide to Logical Verification」や「Natural Numbers Game」なども併せて紹介されている。