数学でAIコードを証明する新興企業が急増
原題: The ‘Pain in the Ass’ Math That Could Save Vibe Coding From Itself
なぜ重要か
AIコード生成が急拡大する中、検証技術の自動化は品質保証の新市場として数億ドル規模の資金を集めており、ソフトウェア開発の信頼性基盤を再定義する可能性がある。
形式検証（formal verification）を自動化するスタートアップが相次いで登場している。&Truth社は2026年10月29日に公式ローンチし、累計7,000万ドルを調達。競合のHarmonicは2億9,500万ドルを調達しAIエージェント「Aristotle」を発表。AnthropicとTheoremも連携し、数兆回のテストで見逃されたバグをAIで発見したと報告した。
ソフトウェアのバグをゼロにする手段として数十年前から存在していた「形式検証」が、生成AIの登場によって実用化の段階に近づきつつある。形式検証とは、数学的な手法でコードが意図通りに動作することを証明するプロセスだ。従来は専門家が5カ月かけて行う作業も、Stanford大学の研究者Chuyue Sunらが開発したAIツールでは500ドル未満・半日以内で完了したという。SunはSignalの暗号化コードの一部を検証する研究成果を論文で発表し、8月に&Truth社に参画した。
&Truth社は同日、7,000万ドルの資金調達を発表してローンチした。最終的にあらゆるプログラミング言語の検証を目指すと説明している。チーフサイエンスオフィサーのIlya Sergeyは「橋や建物が崩壊しないのは、建設前に数学的な検証をしているからだ。コードでも同じことができるのに、スケールが難しかっただけ」と語る。
競合のHarmonicはRobinhoodのCEO、Vlad Tenev氏が共同創業し、累計2億9,500万ドルを調達。今週、AIエージェント「Aristotle」がCで書かれたソフトウェアとVerilogのハードウェア設計の検証に対応すると発表した。NvidiaのベンチャーキャピタルもHarmonicの投資家に名を連ねており、半導体設計会社のTensordyneやNvidiaが評価ユーザーとして挙げられている。
AnthropicとTheoremは先週、AIを活用してオープンソースソフトウェアの未検出バグを発見したと共同発表し、Claudeの拡張機能として他の開発者向けに形式検証支援ツールも公開した。コストは非公開。
ただし課題も多い。技術はいまだプロトタイプ段階にあり、NASAやAppleなど一部の重要システム以外への普及は未知数だ。ユーザーエラーやハードウェア障害に起因するバグへの対処については懐疑的な専門家もいる。顧客がどこまで費用を負担し、どのような形で導入を進めるかも不透明なままだ。