AIが生成したソフトウェアの正しさを検証する自動化ツールを構築する"Theorem"がSeedで$6Mを調達

Theoremは、Khosla Venturesがリードし、Y Combinator、e14、SAIF、Halcyon、エンジェル投資家が参加したSeedで$6Mを調達した。

San Francisco拠点でY CombinatorのSpring 2025バッチから誕生したAIが生成したソフトウェアの正しさを検証する自動化ツールを構築するTheoremは、AIがソフトウェア開発を再構築する中で、業界における次の大きなボトルネックは「コードを書くこと」ではなく、「それを信頼すること」になると賭けています。

この資金調達は重要な転換点で行われました。GitHub、Amazon、Googleといった企業のAIコーディングアシスタントは、すでに年間で数十億行のコードを生成しています。エンタープライズでの導入も加速しています。しかし、AIが書いたソフトウェアが本当に意図した通りに動作するかを検証する能力は追いついていません。その結果、金融システムから電力網に至るまでの重要インフラを脅かす「監督ギャップ」が拡大していると、Theoremの創業者たちは述べています。

Theoremの中核技術は、ソフトウェアが仕様通りに正確に振る舞うことを数学的に証明する形式手法であるformal verificationと、証明を自動生成・検証するように訓練されたAIモデルを組み合わせたものです。このアプローチにより、従来は博士レベルのエンジニアリングを何年も必要としていたプロセスが、同社によれば数週間、あるいは数日で完了できるようになります。

formal verification自体は数十年前から存在していましたが、航空電子機器、原子炉制御、暗号プロトコルといった最重要ミッションクリティカルな用途に限定されてきました。1行のコードに対して8行の数学的証明が必要になることも多く、そのコストの高さが一般的なソフトウェア開発への適用を阻んでいました。

Theoremのシステムは、「fractional proof decomposition」と呼ぶ原理で動作します。複雑なソフトウェアに対して計算量的に不可能な、あらゆる挙動を網羅的にテストする代わりに、コードの各コンポーネントの重要度に応じて検証リソースを配分します。このアプローチにより、Claudeを開発するAnthropicでのテストをすり抜けたバグを最近発見しました。

Theoremはすでに、AI研究所、電子設計自動化、GPUアクセラレーテッドコンピューティング分野の顧客と協業しています。

Theoremは、AIとformal verificationの交差点を探る多数のスタートアップや研究機関が存在する市場に参入しています。同社の差別化要因は、数学など他分野ではなく、ソフトウェア監督のスケーリングに特化している点にあります。

「私たちのツールは、変更をマージする前に正しさの保証を必要とする、低レイヤーに近いシステムエンジニアリングチームにとって有用です」とTheoremの共同創業者は述べています。

Theoremの登場は、エンタープライズの技術リーダーがAIコーディングツールを評価する方法の変化を示しています。AI支援開発の第一波は、生産性向上、すなわち「より多くのコードを、より速く」書くことを約束しました。Theoremは、次の波では別のものが求められると見ています。それは、スピードが安全性を犠牲にしていないことを示す数学的証明です。

AIシステムは指数関数的に改善しています。その軌道が続けば、人間がこれまでに構築したことのないほど複雑なシステムを設計できる、超人的なソフトウェアエンジニアリングが不可避だとTheoremは考えています。

「そして、監督の経済性を根本的に変えない限り、私たちは自分たちで制御できないシステムをデプロイすることになるでしょう」とTheoremの共同創業者は述べています。

機械はコードを書いています。今、その仕事をチェックする誰かが必要なのです。