VerifAIXが500万ドル調達 ― AIが設計した回路をAIでどう「正しい」と証明するのか？

2026年9月16日、AIを活用した検証ソリューションを手がける米VerifAIXが、シード・ラウンドで500万ドルを調達したことが明らかになった。

関連ニュース

VerifAIXは2024年に設立されたスタートアップで、カリフォルニア州クパチーノに本社を置く。

CEOのMadhulima Tewari氏は、Synopsysで半導体設計・検証向けEDAツールに携わったほか、Sun MicrosystemsやNXPでプロセッサ／SoCの設計に従事。その後はIBM WatsonなどAIやエンタープライズ・ソフトウェアの世界でも経験を積んでいる。

共同創業者でチーフ・アーキテクトのKenneth Roe氏はFormal Verificationの専門家で、Intel、SiFive、Synopsysなどで検証技術やFormal Verification環境の開発に携わってきた。Roe氏はJohns Hopkins UniversityでFormal VerificationのPh.D.も取得している。

もう一人の共同創業者Avner Landver氏もApple、Intel、Cadence、IBM Researchなどで検証エンジニアとして25年以上の経験を持つという。また、Intel Pentiumプロセッサの開発で知られるVinod（Vin）Dham氏もFounding Advisorとして同社に参加している。

VerifAIXは、今年のDACで業界デビューを果たしたばかりで、今回同社初となる資金調達で500万ドルのシード資金を調達。インドのベンチャーキャピタルEndiya Partnersと、Deep Techへの投資を手掛けるBluehill VCが共同で資金調達をリードした。

「AIが作ったRTLを、誰が正しいと保証するのか？」

VerifAIXが狙っているのは、生成AI／Agentic AIの普及によって新たに浮上しつつあるチップ設計上の問題だ。

現在、AIは仕様書の解析やRTL生成、アサーション生成、テストベンチ生成、デバッグなど、チップ設計フローのさまざまな領域に入り始めている。しかし、AIがRTLやテストベンチを高速に生成できるようになったとしても、「生成されたものが仕様通りに正しい」ことまで自動的に保証されるわけではない。

AIが生成したRTLを別のLLMにチェックさせても、どちらも確率的に回答を生成するAIである以上、それだけでは「Ground Truth（正解）」を保証できない。

VerifAIX CEOのMadhulima Tewari氏は、この問題を端的に、「Generating a design is not the same as proving that it is correct（設計を生成することと、それが正しいと証明することは同じではない）」と説明している。

そこでVerifAIXが掲げるのが、AIによる設計・検証フローとは独立した「Verification Trust Layer」という考え方だ。

VerifAIXの中心技術「Formal Brain」

「Verification Trust Layer」は、AIが生成したRTLやテストベンチなどを、そのAI自身の判断とは別の根拠で検証するための「信頼性の基盤」と位置付けられるもので、その中心的な技術となるのが「Formal Brain」と呼ぶ仕組みだ。

生成AIによる検証支援では、LLMに仕様書やRTLを読み込ませ、そこからテストベンチやアサーションを生成させる、といったアプローチが一般的にだが、これに対してVerifAIXでは、まずアーキテクチャ仕様、マイクロアーキテクチャ仕様、RTL、既存の検証資産などをまとめて解析し、以下のような情報を抽出。これらを数学的／フォーマルな手法に基づく設計モデルとして構築する。このモデルが「Formal Brain」だ。

• 仕様では何が要求されているのか
• RTLではそれがどのように実装されているのか
• ステートやトランザクションはどう遷移するのか
• 不変条件は何か
• 仕様とRTLに矛盾や抜けがないか

重要なのは、LLM自身に「生成して、その生成結果を自分で正しいと判断させる」のではない点にある。

LLMによる推論や生成結果を、「Formal Brain」を基準として決定的な解析やフォーマル・チェックによって検証することで、AIの出力に独立した根拠を持たせる。つまり、「Formal Brain」を利用することで、「AIがそう判断したから正しい」ではなく、「元の仕様とFormalなモデルに照らして正しい」という状態を目指している。

仕様解析から検証クロージャまで4種類のエージェント

現在VerifAIXが公開しているプラットフォームは、複数のAI Agentによって検証工程をカバーするAgentic AI型の構成になっている。

SpecAI Agent：最初に仕様書とRTLを解析するエージェント

アーキテクチャ仕様からトランザクション、ステート、インバリアントなどを抽出し、RTLと突き合わせる。
仕様に書かれていないRTL動作、矛盾、曖昧な記述、エッジ・ケースなどを検出し、「仕様の抜け」なのか「RTLの実装ミス」なのかを整理する。
ここで構築されたモデルをエンジニアが確認・承認した上で、その後の検証作業に利用する。

TestplanAI Agent：Formal Brainから検証プランとカバレッジ・モデルを生成するエージェント

各要件とテストケースを対応付け、どの仕様がどのテストで確認されるのかを追跡可能な状態にする。
これにより単に大量のテストを実行するのではなく、「仕様のどの要件まで確認できているのか」を追跡できるようにする。

TestbenchAI Agent：テストプランとFormal Brainを基に、実際の検証環境を生成するエージェント

UVM/SystemVerilogベースのテストベンチ雛形生成に加え、アサーション、コンストレインと、スコアボード、チェッカーなども自動生成する。
また生成された検証コードについても、元の仕様やRTLとのトレーサビリティを維持するため、Failureが発生した際に「何を確認するためのテストだったのか」まで追跡可能としている。

VerificationAI Agent

シミュレーションとフォーマル検証を実際に動かしながら検証クロージャを進めるエージェント

既存のシミュレータ、モデル・チェッカー、フォーマル・エンジンなどをAPI経由で操作し、反例の解析、カバレッジ・ホールの特定、根本原因分析、レグレッションなどを繰り返す。

VerifAIXによると、これらエージェントは特定のEDAツールには依存せず、ユーザーが現在利用しているシミュレーション／フォーマル検証環境と組み合わせられる設計になっているという。

興味深いのは、VerifAIXが完全自律型のRTL修正を目指しているわけではない点だ。現時点ではHuman-in-the-loopを前提とし、AI Agentは修正候補や解析結果を提示するものの、仕様やRTLへの変更には人間の承認を必要としている。

EDAツールそのものを置き換えるわけではない

VerifAIXの位置付けを理解する上で重要なのが、Cadence、Synopsys、Siemensなどが提供するシミュレータやフォーマル検証ツールそのものを置き換えることを狙っているわけではないという点だ。

同社のVerificationAI Agentは、既存のシミュレータ、モデル・チェッカー、フォーマル・エンジンなどをAPI経由で利用する「Tool-agnostic」な構成を掲げている。つまりVerifAIXが提供しようとしているのは、新しいシミュレーション・エンジンではなく、検証プロセス全体を横断して管理する「Agentic Layer」と考えた方が分かりやすい。

これは、EDA業界で急速に広がっている「AI Agentが既存EDAツールを使って設計工程を自律的に進める」というAgentic EDAの流れとも一致する。ただし、VerifAIXが特に強調しているのは「自律性」よりも正しさと信頼性だ。

「生成するAI」の次は「検証するAI」

VerifAIXはすでに複数の半導体企業でパイロット・プロジェクトを進めているという。当面は複雑なIPやBlockレベルの検証を中心に展開し、今後サブシステム、さらに大規模なシステムへと対象を広げていく計画だ。「Formal Brain」を大規模設計へ上手くスケールできるかが大きな課題となる。

生成AIによってRTLやテストベンチを短時間で大量に生成できるようになれば、チップ設計におけるボトルネックは「作ること」から「それが本当に正しいか確認すること」に移っていく可能性がある。

EDA各社はAI Agentによる設計・検証自動化を急速に進めているが、VerifAIXが掲げるのは、そのさらに下層に「AIが生成した設計物を信頼するための基盤」を構築するというアプローチだ。

AIが実際に設計作業を担うAgentへ進化すればするほど、「そのAgentの仕事を誰が検証するのか」という問題は避けて通れなくなる。VerifAIXが掲げる「Verification Trust Layer」が、Agentic EDA時代の新しい検証レイヤとして定着するのか、今後の展開が注目される。

VerifAIX