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

Innovation技術部の加藤です。この記事は「Proof Summit 2025 に登壇しました (前編)」の続きです。

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

例題: ロボットのすれ違い問題

図のように、倉庫の間にロボットを置いて、荷物を運搬することを考えます。
ロボットの制御はそれぞれで行い、互いに互いの動きや動作タイミングを知らないとします。
このとき、ロボット同士がぶつかり合わないためにはどうしたらいいでしょうか。

ある設計者は、以下のような設計を考えました。

それぞれのロボットは、「判定」、「進む」、「避ける」のいずれかのアクションを取る

• 判定: 前方1マスに別のロボットがいるか、いないかを判定する
• 進む: 判定の結果、前方にロボットがいない場合は1マス前進する
• 避ける: 判定の結果、前方にロボットがいる場合は1マス横に避ける

設計者は、このようにすることで、ロボット同士が向かい合った状況のときにも上手にすれ違うことができるという風に考えました。

しかし、本当にこれでロボット同士がぶつかり合うことはなくなったでしょうか？TLA+で検証してみましょう。

TLA+では、現在の状態を変数の組で表します。また、動いているプログラムを状態として扱うために、動作中のプログラムが現在どの行を指しているかを表す pc (プログラムカウンタの略) という変数を導入します。今回、ロボットAとBが、それぞれ位置posとプログラムカウンタpcを変数として持つため、状態は以下のように表せます。

プログラムが動くと、pcや変数が変化しますが、それを状態遷移として記述します。
TLA+で状態遷移を記述するのは非常に難解ですが、TLA+には、通常のプログラミング言語に似た構文を持つPlusCalという言語が用意されており、PlusCalをTLA+にトランスパイルすることでTLA+で書かれたモデルとして扱うことができます。

そして、検証したい条件として不変条件 (INVARIANT)である pos["A"] /= pos["B"] を設定します^[1]。

あるいは、状態の列 (つまり、変数の時系列変化) に対して、様相演算子で条件を設定することもできます。主な様相演算子に Always (いつも真になる) と Eventually (いつか真になる) があります。

今回検証したい性質 (PROPERTY) は、様相演算子を使って書くなら、いつも激突しないことなので [] pos["A"] /= pos["B"] となります^[2]。
このようにモデル化をして、TLA+でモデル検査を行うと、TLA+は激突するパターンを発見します。

設計者は、激突しないように設計を変更することができ、バグを未然に防ぐことができます。

応用例: メッセージキューとデータベースを組み合わせた設計のレビュー

もう少し、ITシステムに近い例を考えてみましょう。メッセージキューとは、送信者から受け取ったメッセージを溜め込んで、受信者からのリクエストに応じて溜め込んだメッセージを返すシステムです。

今回は、メッセージキューからメッセージを受け取り、それをデータベースに保存するという単純なシステムを考えます。
このとき、受信者となるシステムに一時的に障害が発生しても、メッセージが保存されなかったり、重複して保存されることがないような設計を考えます。

そのために、まず、メッセージキューはメッセージの再送が出来るよう一度送信したメッセージも削除せずにしばらく残しておきます。また、受信者がメッセージキューに「どこまで受け取ったか」を保存します。これを、Offset Commitと呼ぶことにします^[3]。

しかし、受信者はOffset Commitはどのタイミングで送ればいいのでしょうか?
もしもデータベース書き込み後にOffset Commitを送れば、データベース書き込みが終わってからOffset Commitを送るまでのタイミングで障害が発生すれば、メッセージは重複して保存されます。しかし、メッセージの保存に漏れが発生することはなく、このような、全てのメッセージが少なくとも1回は処理^[4]されるような性質をAt Least Onceと呼びます。

また、受信してすぐの、データベースに書き込む前のタイミングでOffset Commitを送れば、メッセージの保存漏れは防げますが、Offset Commitを送ってからデータベースに書き込むまでの間に障害が発生するとメッセージの保存漏れが発生します。このような「多くとも1回」メッセージが処理されるような性質をAt Most Onceと呼びます。

設計者は、漏れなく重複なくメッセージを処理するために、メッセージに一意的なIDを振り、At Least Onceとなるように処理を行い、また、データベース書き込み時に同じIDのものが既に書き込まれていないかを確認することで重複保存を防ぐことでAt Most Onceを実現する処理を考えました。そのために、以下のような設計書を書きました。

1. メッセージキューからメッセージを受信する
2. データベースのトランザクションを開始する
3. データベースを参照し、既にメッセージが保存されていないかを確認する
4. 保存されていなければ、データベースにメッセージを保存する
5. メッセージキューにOffset Commitを送る
6. データベースのトランザクションをコミットし、変更内容をコミットする

そして、メッセージキューの専門家に、この設計で正しいかをレビューしてもらいます。
この設計は、このようなシステムの設計を経験しているエキスパートから見ると、非常に違和感のある設計です。

1. メッセージキューからメッセージを受信する
2. データベースのトランザクションを開始する
3. データベースを参照し、既にメッセージが保存されていないかを確認する
4. 保存されていなければ、データベースにメッセージを保存する
5. メッセージキューにOffset Commitを送る →データベースのトランザクションをコミットし、変更内容をコミットする
6. データベースのトランザクションをコミットし、変更内容をコミットする →メッセージキューにOffset Commitを送る

のように、5と6を入れ替えないと障害発生時に問題が起こるはずなのですが、具体的にどのような問題が発生するのかを説明するのが少し大変です。

そこで、エキスパートは、TLA+を使って今回の設計をモデル化しました。
そしてモデルを実行し、

• 元の設計ではAt Least Onceが満たされていないことを検証
• 5と6を入れ替えるとAt Least OnceとAt Most Onceが共に満たされることを検証

しました。

さらに、TLA+が見つけ出した反例をGitHub Copilotに与えて、説明スライドを作ってもらいました。

このようにTLA+と生成AIを活用することで、エキスパートは的確で分かりやすいフィードバックを設計者に返すことができました。

企業での形式手法の活用可能性

今回は、短い期間で活用可能性の検討を行ったため、簡単なモデルでの例を試してみましたが、短期間でも十分に面白い結果が得られ、また、特に生成AIとの組み合わせにより、エキスパートレビューでの活用などのユースケースが見えてきました。

今回の検証に参加したメンバーは全員TLA+未経験であるにも関わらず、短期間でTLA+を使えるようになりました。とはいえ、使えるようになるハードルは高く、誰でも簡単に使えるわけではないと感じました。それもあって、今回は、エキスパートがTLA+を書き、動作結果をもとに説明を作成するというユースケースを考えました。設計者もTLA+が分かれば、設計者の方でもモデルを書き換えて、よりよい設計を作れるようになるかもしれません。
生成AIはTLA+をある程度は読み書きすることができるため、学習の手助けや作業の補助には有用です。

また、システム全体を形式手法で検証することは非現実的なため、システムの一部を抜き出し、抽象化し、何が検証出来たら嬉しいかを考える必要があります。活用する上で一番難しいのは、それを見つけることだと感じました。もしかすると、典型的な処理をいくつかモデル化しておくことで、似た処理のものは既にあるモデルを使いまわすなどで乗り越えやすくなるかもしれません。

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

脚注

1. /= はTLA+で「等しくない」を意味する演算子です。

2. [] によって Always を、 <> によって Eventually を表します。

3. Offset CommitはApache Kafkaというシステムで使われる用語で、他のシステムでは、同様の概念をacknowledgementなどの別の用語で表します。

4. この記事では、メッセージの処理とは、データベースへの書き込み(トランザクションのコミット)を指すことにします。