購入フローのテスト組合せ爆発対策で形式検証に入門した

購入フローのテストが組み合わせ爆発で追いつかないという問題に対して、筆者は形式検証（TLA+によるモデル検査）を試した。購入で起きた変更障害を分析すると、取りうる状態やアクションが組み合わさり、実際にはテストしきれず、マイナーな組み合わせで障害が起きることが多いという傾向があった。決済を挟んで取引（TX）が何段にも分かれ、TX単体のテストは通っても、TX間の事前条件・事後条件が噛み合わず、終端に辿り着けないケースが目立つ。

面白いのは、形式検証で見つかった問題の性質だ。期限切れ補償の処理では、決済側の補償が成功したあとに注文側の補償が失敗すると、リトライ時に「変化なし（NoChange）」が返り、補償がスキップされて注文が進行中のまま残ってしまう。つまり冪等でない処理が不整合を生むという指摘である。もう一つは、アクションを特定の回数や順序で実行したときにだけ崩れる問題で、正常系のシナリオを書いているだけでは気づきにくい。TLAは本来アクションを繰り返し実行する前提で探索するため、こうした「二度目に起きること」を拾える。業界的には、テストケースを人間が列挙する限界を、仕様の宣言によって越えようとする試みだと読める。ただし、この検証が効いたのは、補償を別アクションとして切り出したという人間側の設計判断があったからだ。AI任せでは、その切り出しが抜け落ちる危険もある。

実務への含意としては、すべての変更に形式検証を当てる必要はない。筆者も、AIに同じ監査手順を踏ませるだけで多くの課題が見つかるため、組織展開では形式検証を外した監査ワークフローを提供する方針だという。ただし1回の監査で数百kトークンを使う点は、コストの見積もりに入れるべきだ。決済や返金といった補償処理を含む改修など、ミスの代償が大きい変更にだけ形式検証を当てるのが現実的だろう。