AIで形式検証は普及するか、スタートアップが参入し期待と懸念が交錯

形式検証は、ソフトウェアの目標を厳密に記述し、コードを検証可能な数式に変換して正しさを確かめる手法である。従来は時間がかかり、NASAやApple、Boeing、Amazonなど限られた重要システムでの利用にとどまってきた。Chuyue Sunらは、Signalの暗号化コードの一部をAIで検証し、専門家3人が5カ月かけた作業を半日未満、500ドル未満で終えたと論文で報告した。

この結果を受けて、スタートアップが相次いで参入している。&Truthは7000万ドルを調達し、将来はあらゆるプログラミング言語の検証を目指す。Harmonicは2億9500万ドルを調達しており、AIエージェントAristotleがCのソフトウェアとVerilogのハードウェア設計の検証に対応したと発表した。Anthropicと検証スタートアップのTheoremは、AIを使って既存テストで見つからなかったバグを発見し、Claude向けのアドオンも公開した。Truidicも新たに加わった。

懐疑的な声もある。Antithesisのウィルソン氏は形式検証を「罠」と呼び、検証には大きな手間がかかる上、網羅的なテストこそが保証を裏づけると述べる。Vitalik Buterinも万能ではないと指摘している。中堅企業は、検証担当者の不足やコスト、検証待ちによる開発の遅れを理由に、重要機能の一部しか検証していないという。

今後の焦点は、資金と提供形態である。オープンソース保守者は継続的な資金源が見えないと話し、スタートアップは顧客に直接提供するか、Anthropicのような仲介を使うかを決めかねている。Proofcraftには問い合わせが殺到しているが、AIが生成する仕様が「不当な信頼」を生む恐れも指摘している。