&Truth、コード向け汎用検証マシンの開発に向け7,000万ドルのシード資金を調達

ソフトウェアの安全性を数学的に証明する技術を開発する公益法人の&Truthは、2026年10月29日にステルス状態を脱し、7,000万ドルのシード資金を調達したことと、同社が「コード向け汎用検証マシン」と呼ぶものを開発する計画を明らかにした。

創業発表によると、同社は2026年初頭に設立され、AI安全性とベンチャーキャピタルの分野を切り開いてきたと同社が評するリーダーたちから、7,000万ドルのシード資金を調達した。同社は、あらゆるプログラミング言語のコードを読み取り、安全性、セキュリティ、正しさを数学的に証明する検証マシンを開発しており、証明は誰でも独立して検証できるとしている。

Leanを基盤とする証明の自動化

発表によると、形式検証は数十年にわたって存在してきたものの、専門家が証明を手作業で定式化する必要があったため、これまでは利用が難しく、費用も高かった。その結果、適用対象はごく少数の重要システムに限られていた。同社によると、AIによって形式証明の作業は現在、100倍以上加速しており、同社の証明自動化技術はそのプロセスをさらに100倍加速させる。これにより、証明の生成に数年から数カ月かかっていたものが、数時間から数分で済むようになるという。

同社はまた、「仕様ファクトリー」と呼ぶ技術についても説明した。同社によると、この技術により企業や開発者は、人間の意図やビジネス要件を大規模に、厳密な形式仕様へと変換できる。これにより、テストやベンダーの主張に頼るのではなく、独立して検証可能な保証を提供できるという。

&Truthは、オープンソースの証明システムであるLeanと、200万行を超える数学的定義や定理を収録したライブラリMathlibを基盤として開発を進めており、CSLibをはじめとするオープンソース技術も活用している。同社が目指すのは、ソフトウェアに共通する汎用的な形式言語だ。これには、プログラミング言語やシステムの数学的モデル、証明手法、そして言語をまたいだ自動検証を可能にする厳密な仕様が含まれる。&Truthは、Lean Focused Research Organizationと連携しており、基盤となるライブラリをオープンソースとして公開する意向を示している。

共同創業者兼共同CEOのClark Barrettは、LeanとMathlibによってAIは数学的推論に使える厳密な言語を得た一方、ソフトウェアには同等の基盤が欠けていると述べた。共同創業者兼最高科学責任者のIlya Sergeyは、ソフトウェアへの信頼は企業の言葉ではなく、独立して検証可能な証明に基づくべきだと語った。

創業者と2カ所の本社

Barrettは、Stanford UniversityのCorbelコンピューターサイエンス教授であり、Stanford Center for AI Safetyの創設時からの共同所長、Stanford Center for Automated Reasoningの所長、CSLibの共同開発者、そして自動推論エンジンcvc5のプロジェクトリーダーを務める。SergeyはNational University of SingaporeにVERSE Labを設立し、オープンソースの検証ツールVeilとVelvetを共同開発した。共同創業者兼共同CEO、取締役会長のChris Hsuは、Lean FRO Strategic Advisory Boardのメンバーであり、Infinitude Foundationの会長を務める。それ以前には、Kilometre CapitalのCEOおよびCitadel Investment Groupのマネージングディレクターを務めた。

発表では、BlueRock Securityで形式手法部門を率い、検証フレームワークBRiCkの主要設計者を務めたGregory Malecha、Lean 4の共同設計者でLean Focused Research Organizationの共同創業者でもあるSebastian Ullrich、Kilometre Capitalの元マネージングパートナーであるLinus Lee、そしてFastino Labsの元最高商務責任者で、Insight PartnersとShasta Venturesのオペレーティングパートナーを務めたDrew Harmanも紹介された。&Truthは、Stanford UniversityとNational University of Singaporeにおける形式検証および自動推論の数十年にわたる研究を基盤としていると述べた。

&Truthの米国本社はPalo Altoに、国際本社はSingaporeにある。同社によると、Singaporeのオフィスでは、研究、エンジニアリング、製品、市場開拓の各業務を大幅に拡大する予定だ。Singaporeのデジタル産業担当上級副社長兼共同責任者であるLow Jin Yongは発表の中で、この本社設置によってSingaporeの信頼性と安全性に関する能力が高まり、信頼できるAIを開発する企業にとって同国が拠点としてさらに強化されると述べた。

同社のウェブサイトでは、Leanの発明者でAWSの副社長兼特別研究員であるLeonardo de Mouraと、Lean FRO Strategic Advisory BoardのメンバーでGoogleの特別技術者であるSimone Severiniによる座談会も紹介されている。

付随する論考で同社の開発理由を詳述

2026年10月29日付の関連論考でHsuは、検証が急務だと同社が考える背景にある動向を詳しく説明した。その中で、GoogleのCEOであるSundar Pichaiの発言を引用し、Googleでは新たに書かれるコードの75%が現在AIによって生成され、エンジニアの承認を受けていると述べた。また、Veracodeが2026年に実施したテストでは、セキュリティが重要となるコーディングタスクのほぼ半数でAIモデルが失敗したという。さらに論考では、攻撃者がAIエージェントを数百個展開し、広く使われている印刷管理ソフトウェアの脆弱性を突いて48カ国の395組織に侵入した2026年9月の攻撃キャンペーンと、2026年9月に公表されたソフトウェア脆弱性が過去最多の14,959件に達したことも挙げている。同論考によると、この件数は前年の同時期に公表された数の3.5倍に当たる。

このエッセイは、形式検証における過去の節目を振り返っている。seL4マイクロカーネルの最初の証明には、約8,700行のコードに対し、専門家の作業時間でおよそ20人年を要した。2015年には、DARPAのHACMSプログラムのもと、seL4がBoeingの無人ヘリコプター「Unmanned Little Bird」に組み込まれた。数週間にわたりアクセス権を与えられたプロのレッドチームも、その飛行制御を突破できなかった。また2026年9月には、Anthropicが開発したAIモデルが、フェルマーの最終定理の完全な証明をLeanで形式化するのに11日を要した。さらに、2026年初めにはLean FROのシニア・リサーチソフトウェアエンジニアであるKim Morrisonが、AnthropicのClaudeを使い、人間による最小限の指示のもとでLean版のzlib圧縮ライブラリを構築し、圧縮したデータを常に元のまま正確に復元できることを証明したと記している。

このエッセイでは、Leanの開発者であるLeonardo de Mouraの言葉を引用している。「テストは確信を与える。証明は保証を与える。」

2026年10月29日に公開された2本目のエッセイで、Sergeyはプログラム検証の仕組みを解説している。まず取り上げるのは、プログラマーがコードに、検査器が個別に検証できる正確な主張を添えることを提案した、Alan Turingの1949年の論文「大規模ルーチンの検査」だ。エッセイでは、仕様、ループ不変条件、Leanで検査する証明について説明し、開発者がLeanによる形式証明などの、第三者が独立して検査できる証拠を、検証を開発工程の通常の一部にできるコストで得られるようにすることが、&Truthの目標だと述べている。

&Truthは長期的なビジョンとして、「雰囲気コーディング」から「検証コーディング」への移行を掲げている。そこでは、AIが生成したコードをデプロイ前に数学的に検証し、AIエージェントは安全に隔離されていることを証明できる環境内で動作し、レガシーソフトウェアは安全に近代化され、重要インフラは第三者が独立して検査できる数学的保証によって保護される。