「バイブ形式手法」: 実装から仕様を吸い出し、Z3／TLA+ で反例を探して CI に載せる

どんな場面で使う？

• 設定・ルール・権限判定など「どんな入力でも成り立つべき条件」がある
• 上限チェック、カウンタ、リトライ、非同期の記録など、同時実行や順序で壊れそうな処理がある
• AI が書いたコードを1行ずつ読まずに、性質の保証を取りたい

手順（@mizchi の手順書から要約）

1. 道具を選ぶ: 「どんな入力でも成り立つ？」→ Z3。「どの順で起きても・同時に来ても・クラッシュ後も大丈夫？」→ TLA+。状態が有限で決定的なら、まず素の全列挙。認証認可はたまに Alloy、アルゴリズム自体の正しさを示したいときは Lean（@mizchi の使い分け）
2. 実装を読ませて2種類に分けて抜き出す: コメント・テスト名・ガード節・enum などの「宣言された仕様」と、既定値・空や nil の扱い・エラー時の倒れ方・評価順などの「暗黙の挙動」
3. 各判定に機械的に問いを投げる: 空なら？ 取得失敗なら true／false／例外のどれ？ 否定をかけると？ 境界は > か >= か？ 同時に2つ来たら？ その値を決めるのは誰か（信頼できない入力か）？ ループは何で止まる？
4. 純粋な判定関数と、名前付きの不変条件を書く: 例 NeverOverCap == served <= cap。成立を示したいのか反例が欲しいのかを決める
5. 回す: 反例が出たら具体例つきで「意図か？」を確認 → 意図なら仕様として明文化、違えばバグ。成立したら回帰ガードとして固定
6. CI に載せる: 期待（VIOLATE／OK）と一致するかを assert するモードを持たせる。わざと壊した実装（ガードを外す等）を用意し、検査が赤くなることも確かめる。ソルバー等の依存は lockfile／nix などで固定。fuzzing・PBT で同じ入力をモデルと実装に流し、出力一致を CI で見る

注意点

• 形式手法が検証するのは「書いたモデル」であってコードそのものではない。設定データのように実データを直接食わせられる対象はずれが小さく、命令型・並行コードは手で抽象化するぶんずれが大きい。実システムのイベントログをモデルに再生して確かめる（trace-checking）とずれを詰められる
• 実装を読まずに記憶や要約からモデルを組ませると、偽の証明になる（変換表1つの取り違えで崩れる）。「常に緑」は何も検証していない可能性がある
• 確率的な性質、制御理論的なもの、すでに総当たりテスト済みの最適化は向かない。主要な不変条件と危険な穴を押さえたら、新しい形式化より溜まった反例・確認質問の処理を優先する
• まずは決済・権限・在庫など、壊れると困る部分だけから始める（@mizchi も段階的な形式化を推している）
• 関連: ガイド: AIコーディング（エージェント運用 / プロンプト / マルチモデル）

出典

• @mizchi · 2026-10-23 ／ @mizchi · 2026-10-23
• 手順書（gist）: gist.github.com