Lean で学ぶ形式検証入門（第1回）
Original : Introduction to Formal Verification with Lean Part 1
Pourquoi c'est important
形式検証と暗号技術の実践的な橋渡しとして、開発者教育に貢献する取り組み。
HashCloak の暗号技術エンジニア Elena が、定理証明支援系 Lean 4 を用いた形式検証の入門チュートリアルを公開した。暗号プロトコル「One-Time Pad」の形式的証明を題材に、Lean の基礎から解説する全4部構成の第1回。
HashCloak のブログにて、暗号技術エンジニアの Elena が Lean 4 を使った形式検証の入門チュートリアル（第1回）を2026年7月15日に公開した。形式検証とは、数学的な命題の正しさをコードで記述し機械的に検証する手法で、Rocq（旧Coq）、Isabelle、Lean などのツールが代表例として挙げられる。本チュートリアルは、形式検証の経験が浅い暗号技術者を主な対象とし、Claude Shannon が広めた One-Time Pad（OTP）プロトコルの形式的証明を通じて Lean の基礎を習得することを目指す。定義と証明の参考資料には Dan Boneh・Victor Shoup 著「A Graduate Course in Applied Cryptography」を使用。Lean は2013年に Microsoft Research の Leonardo de Moura が開発した純粋関数型プログラミング言語かつ定理証明支援系であり、証明のモジュール化や自動補完機能を備える。チュートリアルは「Hello World!」を含む全4部構成で、すべて Lean 4 を使用する。