形式手法（Formal Methods）

仕様や設計を数学的に厳密な形で書き、その性質を機械で検査する技術群。AI コード生成の普及で再評価され、LLM に形式化させて検査器に判定させる使い方が実用になっている

概要

形式手法（Formal Methods）は、仕様や設計を数学的に厳密な形で書き、その性質を機械で検査する技術群。テストが「人間が選んだ入力で正しく動くか」を確かめるのに対し、形式手法の検査器はモデルのすべての入力・すべての実行順を調べ、性質を破る反例を 1 つ返すか「反例なし」と答える。テストが「実装が仕様どおりか」を見るのに対し、形式手法は「仕様そのものが正しいか」まで検査できる。型システムも軽量な形式手法の一種である。

詳細

テストとの違い

	テスト	形式手法
調べる範囲	人間が選んだ入力・実行順	モデルの全入力・全実行順（有限の範囲内）
対象	実装	仕様・設計のモデル
答え	通った／落ちた	反例／「反例なし」
弱点	選ばなかったケースは調べない	モデルが実装と食い違えば結果も外れる

検査器が保証するのは「このモデルについて」の結果にすぎない。そのため、反例は必ず実装のテストで再現させてからバグと判断する。

道具の選び方

道具は「問いの形」で選び、反例を出せる最小の道具を使う。mizchi さんの仕様化スキル formal-methods-reconciler の分類に沿うと次のとおり。

問いの形	例	道具
純粋な述語（入力 → 真偽）	料金計算、設定値の組み合わせ	Z3（SMT ソルバ）
関係（ユーザー・ロール・リソース）	権限、テナント分離	Alloy
状態遷移・並行実行	キャッシュ、リトライ、分散プロトコル	TLA+（モデル検査器 TLC）、Quint
事前・事後条件つきの逐次コード	ループ不変条件	Dafny
無限の範囲での定理	アルゴリズムの正しさ	Lean、Rocq

同スキルは「Z3 で時相的なインターリーブを扱うな」「単純な述語に TLA+ を使うな」とも戒めている。mizchi さんの経験則では、マイクロサービスやマルチスレッドのキャッシュ制御には「ほぼ確実に漏れがある」ので TLA+ か Quint、迷ったら Z3 か TLA+。

Z3：性質の否定を制約として与え、「破る入力はあるか」と問う。sat なら返った値が反例、unsat なら全入力で性質が成り立つ。反例は 1 つずつしか返らないので、既知の反例の種類を除外して問い直す
TLA+ / TLC：状態変数と、1 ステップずつ原子的に起きるアクションでシステムを書き、不変条件を TLC に検査させる。違反すると、初期状態から違反に至る実行順（トレース）が返る

LLM との役割分担

基本姿勢は「LLM がモデルを提案・修正し、検査器が判定する」（formal-methods-reconciler）。

人間：仕様・設計を自然言語で書き、意図した挙動か・バグか・仕様の矛盾かを決める
LLM（Claude Code など）：主張の抽出、形式化、反例の説明、修正案、例え話での説明
検査器（Z3、TLC など）：正しさの判定。LLM の「問題ありません」は判定にならない

mizchi さんが挙げるプロンプト例は、「今あるコードを形式化できる部分を形式化して、それをテストオラクルに、実装がそれに従ってるか確認して」「モデル検査で反例が出たら、それを実際のテストケースに落として」「何を検査したか、ドメインの言葉を使わずに例え話で説明して」。

実践で効く 4 つの規律

反例は実装で再現させる：同じ入力・同じ実行順をテストで強制する。並行実行なら threading.Event などで止める位置を作り、トレースの順番どおりに割り込ませる。再現しなければ、まずモデルの前提（原子性、ロック、リトライ）を疑う
「反例なし」は空振りを疑う：性質が自明に成り立っていないか（例：キャッシュに一度も値が入らない）、前提が一度も真にならないか（例：誰も終わらない）を確かめる。「破られるべき」不変条件を置いて違反が出ること、修正を外した変異版が落ちることをセットで見る。考え方はミューテーションテストと同じ
性質は 1 つだけで検査しない：ある規則だけを検査して unsat を得た修正が、別の規則を黙って破っていることがある。仕様全体を同時に満たせない入力を探す（Z3 なら ForAll で「どんな出力でも全規則を満たせない入力」を求める）と、仕様そのものの矛盾が見える
仕様の矛盾は人間に返す：どう実装しても満たせない仕様は実装側で直せない。決まるまで pytest の xfail(strict=True) で記録しておくと、判断が入って挙動が変わったときに XPASS で気づける

実例（2026-10 の検証）

Z3 × 料金計算：「会員 10% 引き（切り捨て）」「3,000 円以上でクーポン 1,000 円引き」「最終金額は注文額の 60% 以上」の 3 規則。会員がクーポンを使う 3,000〜3,334 円で下限を割る実装バグに加え、1〜2 円の会員注文では切り捨てと下限が両立しない仕様の矛盾が見つかった
TLA+ × キャッシュ無効化：「DB 更新後にキャッシュ削除」の設計で、読み込み側が古い値を読んだあと、更新と削除が先に走り、最後に古い値が書き戻される 5 ステップの競合を TLC が検出。memcached のリース（“Scaling Memcache at Facebook”、NSDI 2013）と同じ考え方の修正で、212,675 状態を網羅して違反なしを確認した

仕様レビューの検査役として使う

要求仕様書作成ループでは、エージェント同士の仕様レビューに Formal Checker を置き、対象を 3 つに絞る — 決定表・計算ルールは Z3（どのルールにも当てはまらない入力＝抜け、2 つのルールが違う結果を出す入力＝矛盾）、並行・リトライ・取り消しが絡む業務フローは TLA+、権限・ロールは Alloy。画面や文言、順番どおりに進むだけのフローは対象外。反例は具体的な入力なので、利用者には式を見せず「A と B のどちらにしますか？」という選択肢付きの質問に直して Q&A 表に起票する。形式手法が確かめるのは仕様内部の整合性だけで、「利用者が本当に必要としているか」は判定できない。

なぜ今なのか（verification bottleneck）

人間がコードを書く時代、形式手法は二重コストだった。形式検証されたマイクロカーネル seL4 は、8,700 行の C コードの検証に 25 人年を要している。

AI エージェントがコード生成を担うと構図が逆転する。

コード生成コスト → AI が担い劇的に低下
コード検証コスト → 人間が担い相対的に増大

人間のレビューが最大のボトルネック（verification bottleneck）になり、かつてコスト超過で退けられた形式手法が相対的に実用的な選択肢になった。金融テクノロジー企業 Jane Street の技術責任者 Yaron Minsky が、25 年間の懐疑を捨てて専門チームを新設したことで再注目された。同社は OxCaml（社内版 OCaml）の型システムを深くコントロールしつつ、Lean・Dafny・Rocq（旧 Coq）を補完として位置づけている。

形式手法は AI 自身へのフィードバック機構にもなる。「テストが通った」は曖昧な信号だが、「すべての入力で成立する」は普遍的な保証であり、AI 生成コードを評価・改善するループの停止条件として使える。