JPYCv2 形式検証宣言カタログ

このサイトについて ​

jcam1/JPYCv2（UUPS プロキシ・FiatToken 系の 日本円ステーブルコイン）の検証対象 FiatTokenV2 を、Lean 4 + Mathlib で 形式検証したプロジェクトの宣言カタログです。Lean モデルに含まれる ソース由来の全宣言（定義・定理・構造体など 392 件）について、1 宣言 1 ページで

• 型シグネチャと和訳した docstring、
• 非専門家向けの解説（何を述べているか／直感／なぜ安全性に効くか）、
• 図解（Mermaid）、
• 検証済みの Lean ソース（証明本文を含む）と対応する Solidity スニペット、
• 関連宣言へのリンク

を掲載しています。

ページの一覧と並び順は、Lean の環境反映で生成される catalog.json から自動生成されるため、ドキュメントが証明から静かに乖離することはありません。

読み方 ​

• 形式検証や Lean になじみがない場合は、まず 形式手法 入門・用語集 を読んでください。Except/revert モデル、 U256/BitVec、WF、SupplyConserved、SigOracle といった共通概念を やさしく説明しています。各宣言ページの専門用語は、この入門のセクションに リンクしています。
• 個々の宣言は、左サイドバーからモジュール（Foundation / ERC20 / AccessControl / Signatures / Upgradeability）ごとに辿れます。ページ下部の「前の宣言 / 次の宣言」で ソース順に読み進めることもできます。
• 検証で「証明していること／していないこと（スコープ外の前提）」は、 検証レポート と入門の該当節にまとめています。