Proof Summit 2025 に登壇しました (前編)

Innovation技術部の加藤です。皆さんは形式手法ってご存知でしょうか。

形式手法は、システムの仕様や動作を数理モデルとして記述し、その正確性を機械的に検証する技術です。専門的であり、まだ実社会での応用はそれほど多くありませんが、並行性や非同期処理の不整合検出に優れており、高信頼性が要求されるシステムの検証に有用であり、今後はシステム開発に不可欠な技術となっていくかもしれません。

今回、私たちは、自社で形式手法を適用できる可能性を探るため、短期間で検証を行いました。そして、その成果を国立情報学研究所(NII)の会議室で開催されたProof Summit 2025で発表してきました。その内容を簡単に振り返ろうと思います。

思ったよりも長くなったので、前編と後編に分けます。
前編では、今回の検証の位置づけや、なぜ今、形式検証に取り組んだのかをお話しします。
後編では、実際に取り組んだ検証課題の紹介を行います。

今回の検証の位置づけ

NTTデータは、公共・金融・法人など多様な業界の基幹システム構築に長年携わってきました。その中には、もしシステムダウンや不具合が起こると社会的にも大きな損害が発生するような、ミッションクリティカルなシステムも多くあります。

私の所属するInnovation技術部は、基幹システムの開発に直接携わるわけではありませんが、新規技術開拓や、そのビジネス適用を通じて、先進技術を他社より先んじて事業価値に変えることをミッションとしています。私は普段は量子コンピューティングや数理最適化などの研究開発を行っていますが、今回、それに並行し、本稿で紹介する形式手法の検証も実施しました。

なぜ今、形式手法が必要か

形式手法は、新しい技術ではなく、古くからアカデミアを中心に研究が進められてきた分野です。これまでにも組み込み系などで一部導入もされていますが、ITシステムの開発には、現状はあまり活用が進んでいませんでした。

しかし、ITシステム開発において、今後は形式手法の必要性が増すのではないかと私は考えており、今回の検証の実施に至りました。その背景としては以下が挙げられます。

モダナイゼーションにおける課題解決

現在、高信頼性が必要なシステムを、メインフレームからオープン系やクラウドに置き換えるなどのモダナイゼーションが各社で進められています。その際、たとえば、当時の設計者の引退や、他社が開発したシステムの置き換えなどにより、当時の設計意図が不明な仕様が出てきます。形式手法により現在の仕様をモデル化すれば、その仕様でなければ何か問題が起こるか、本当にその仕様で問題がないかを検証できます。

システムの複雑化

従来のシステムとは異なり、近年のシステムはリアルタイムに処理されること、並列・非同期で処理されることが当たり前になりつつあります。また、マイクロサービスを用いたアーキテクチャーも普及してきましたが、それにより、サービス間通信が発生し、メッセージの順序が入れ替わったり、欠損が発生するなどの新たな不具合も考えられます。

生成AIの普及

近年、GitHub CopilotやClaude Codeなどのコーディングエージェントが急速に発展し、普及してきています。その生産性向上により、これからのシステム開発では、ソースコードを書くことよりも、ソースコードをレビューすること、検証することの負担が大きくなると考えられます。そこで、テストやCI/CDの一環として、形式手法を取り込めば、AIで生成されたコードを活用しながら信頼性の向上に取り組めるかもしれません。

また、従来、形式手法の普及が進んでいなかった背景に、学習のハードルが高いことや、利用に工数がかかり高コストとなることがありました。これらは生成AIの活用で大きく軽減できる可能性が高く、形式手法普及のための地盤は出来つつあると言えるでしょう。

形式手法の二大方式

形式手法には、大きく分けて2つの方式があります。ひとつが定理証明支援系で、もうひとつがモデル検査です。私たちは両方の方式を検討しましたが、今回の検証範囲では、モデル検査が、よりビジネス適用を行いやすいという考えに至り、TLA+というモデル検査言語を利用することにしました。

定理証明支援系

定理証明支援系は、検証したい性質を数学の「定理」の形で書き、その「証明」をプログラムとして構築することで、検証したい性質の正しさを保証する方法です。
この手法は非常に強力で、特に、組み合わせ爆発を起こすような膨大な入力や、無限に大きな入力に対する性質も、数学的に正しいことを証明することができます。また、「証明」として具体的なアルゴリズムを構築することで、証明から、実際に動くプログラムを抽出することもできます。
定理証明支援系にはRocq (Coqから改名), Agda, Isabelle, Idris, LEANなどがあり、最近は、その中でも後発のLEANの人気が高まってきています。

モデル検査

モデル検査は、検証したい性質とシステムの状態遷移をモデル化し、機械的に状態遷移を探索することで、検証したい性質の正しさを保証する方法です。
この手法は、定理証明支援系と異なり、モデル化さえ行えば証明を行う必要がありません。その反面、機械的に探索を行うので、無限にある入力や組み合わせ爆発を起こす多くの入力は、基本的には扱うことができません。また、モデル検査では具体的な情報遷移を探索することで検証を行うので、検証に失敗した場合は、検証に失敗する具体的な反例を得ることができ、設計へのフィードバックを行いやすいことは大きな利点です。
モデル検査のための言語にはTLA+, Alloy, SPIN, NuSMVなどがあります。TLA+は近年最も勢いのあるモデリング言語やツール^[1]のひとつで、2023年にはLinux FoundationがTLA+ Foundationの発足を発表しました。

ここまでのまとめ

前編では、形式手法とは何か、なぜ企業研究者が形式手法に取り組んだのか、その背景を述べました。
後編では、TLA+を使って具体的にどういった検証を行ったかを紹介します。

https://zenn.dev/nttdata_tech/articles/8d1a28e41b1177?t

今回の検証は、現・OSSソリューション統括部の倉本さん、NTTデータ数理システムさん、proof ninjaさんといっしょに行いました。お忙しい中、ご協力いただきありがとうございました。

脚注

1. TLA+とは形式記述言語の名前であり、プログラムをTLA+で記述するのを補助する言語であるPlusCalや、TLA+で書かれた仕様を検証するツールであるTLC Model Checker、PlusCalをTLA+に変換するプログラムなどは、厳密にはTLA+とは呼びません。しかし、この記事や後編の記事では、それらを区別せず、TLA+やPlusCalに関連するツールも含めてTLA+と記述します。