AIがコードを書く時代になると、「プログラムを作る技術」よりも「プログラムが正しいと保証する技術」の重要性が増す——そう主張する記事が、金融テクノロジー企業 Jane Street のブログに掲載された。著者は同社 Head of Technology（技術責任者）の Yaron Minsky だ。25年間抱いてきた形式手法への懐疑を捨て、専門チームを新設したことを発表している。
形式手法とは何か
形式手法（Formal Methods）とは、ソフトウェアの正しさを数学的に証明するための技術群です。通常のテストが「多くのケースで正しく動くことを確認する」のに対し、形式手法は「ある性質が常に成立することを証明する」ことを目指します。
身近な例を挙げると、型システムも軽量な形式手法の一種です。型チェッカーが「この関数に文字列を渡すことは不可能」と保証するのと同じ原理で、より強力な形式検証ツールは「このプログラムはデッドロックしない」「このアルゴリズムは常に終了する」といった性質を数学的に証明します。
コストが高すぎた——25年間の懐疑
Jane Street は OCaml（現在は社内で OxCaml と呼ばれる）の強力な型システムを長年活用してきた企業であり、形式手法の概念自体は熟知していました。しかし Minsky は長らく、ほとんどのソフトウェア開発において形式手法はコストに見合わないと判断していました。
その代表例として挙げられるのが、形式検証されたマイクロカーネル seL4 です。わずか 8,700 行の C コードを検証するために、25 人年もの工数が必要でした。これでは大規模な商用ソフトウェアへの適用は現実的ではありません。
AI エージェントが変えた経済性
状況を変えたのは、AI エージェントによるコード生成の台頭です。Minsky はこの変化を verification bottleneck（検証のボトルネック） という言葉で表現しています。
従来の開発では、人間がコードを書くこと自体に多くの時間が費やされていました。その上にさらに証明を書く形式手法は、二重のコストとして現実的ではありませんでした。
しかし AI がコード生成を担うようになると、構図が逆転する。
- コード生成コスト → AI が担い、劇的に低下
- コード検証コスト → 人間が担い、相対的に増大
AI エージェントが生成するコードは、バグを含んでいたり、コードベースの不変条件（invariants）を守っていなかったりします。そのコードを人間がレビューし、正しさを保証するプロセスが最大のボトルネックになるのです。
形式手法はフィードバックループにもなる
Minsky が指摘するもう一つの重要な視点は、形式手法が AI 自身を賢くするためのフィードバック機構 としても機能する点です。
AI モデルはフィードバックを受けながら改善されますが、「テストが通った」というフィードバックは曖昧です。特定のケースでは正しく動くが、別のケースでは誤動作する可能性を排除できません。
一方、形式手法は「この性質がすべての入力に対して成立する」という 普遍的な保証 を与えます。これはテストよりも厳密なフィードバックであり、AI が生成したコードを評価・改善するための学習環境として機能する可能性があります。
Jane Street の具体的な動き
Jane Street は以下の強みを活かして形式手法に本格的に取り組む方針を示しています：
- OxCaml への深いコントロール——型システムの拡張や実験が可能
- プログラマーコミュニティの高いエンゲージメント——先進的な型システム機能への積極的な関与
- 既存ツールとの連携——Lean、Dafny、Rocq（旧 Coq）といった外部形式検証ツールを競合ではなく補完として位置づける
ロンドンとニューヨークで形式手法の専門チームの採用も開始しており、技術的進化だけでなく組織的なコミットメントを明確にしている。
まとめ
AI コード生成の普及は、ソフトウェア開発の経済性を根本から変えつつある。コードを書くことが安くなる一方で、そのコードを信頼できると証明することのコストが相対的に高くなる——この構造変化が、かつてコスト超過として退けられていた形式手法を、実用的な選択肢へと押し上げている。
Jane Street の動きは、金融業界の最前線で働くエンジニアたちが「AIと形式手法の組み合わせ」に真剣な可能性を見出している証左だ。
参照: