概要
形式手法（Formal Methods）は、ソフトウェアの正しさを数学的に証明する技術群。通常のテストが「多くのケースで正しく動くことを確認する」のに対し、形式手法は「ある性質が常に成立することを証明する」。型システムも軽量な形式手法の一種で、より強力な形式検証ツールは「デッドロックしない」「常に終了する」といった性質を証明する。金融テクノロジー企業 Jane Street の技術責任者 Yaron Minsky が、25年間の懐疑を捨てて専門チームを新設したことで再注目された。
詳細
なぜコストが高すぎたのか
代表例が形式検証されたマイクロカーネル seL4 で、わずか 8,700 行の C コードの検証に 25人年 を要した。人間がコードを書く時代には、その上にさらに証明を書く形式手法は二重コストとして非現実的だった。
AI が経済性を反転させた（verification bottleneck）
AI エージェントがコード生成を担うと構図が逆転する。
- コード生成コスト → AI が担い劇的に低下
- コード検証コスト → 人間が担い相対的に増大
AI が生成するコードはバグや不変条件（invariants）違反を含みうる。それを人間がレビューして正しさを保証するプロセスが最大のボトルネック（=verification bottleneck）になる。かつてコスト超過で退けられた形式手法が、相対的に実用的な選択肢へ押し上げられた。
フィードバックループとしての形式手法
形式手法は AI 自身を賢くするフィードバック機構にもなる。「テストが通った」は曖昧なフィードバックだが、形式手法は「すべての入力に対して成立する」という 普遍的な保証 を与える。テストより厳密なこの信号は、AI 生成コードを評価・改善する学習環境として機能しうる。
関連ツール
Jane Street は OxCaml（社内版 OCaml）の型システムを深くコントロールしつつ、Lean・Dafny・Rocq（旧 Coq）といった外部形式検証ツールを競合ではなく補完として位置づけている。
関連ページ
- ハーネスエンジニアリング — AI 出力の品質を検証層で保証する設計との関係
- AI エージェントにリファクタさせる時の完了の定義 — 「正しいコード」と「安全な変更」を分ける検証境界の話
- スケーラブルオーバーサイト — AI の出力を人間がどう監督するか
ソース記事
- AIコード生成時代に形式手法が実用段階へ——Jane Street が語る検証ボトルネック — 2026-06-24