信頼性の高い設計を形式手法のTLA+とVibe Codingで作成しようとしてみた

概要

この記事ではTLA+を使ったテンプレートを作成し、その上でRoo CodeにVibe Codingさせることで、信頼性の高いビジネスロジックの設計を行おうと試みました。

モデルはgemini-2.5-pro-exp-03-25を用いました (お財布に優しい！)。

結果として、残念ながら実用的な複雑度を持った仕様はとても得られませんでした。ただし、簡単な仕様であれば、TLA+を用いたモデル検査を経た堅牢な状態を得ることができました。

今回用いたコード

これが欲しい人が多いと思いますので先んじて貼っておきます。指定のファイルに仕様を記述してスクリプトを実行すると、その仕様に矛盾がないかを検証できます。詳細な使い方はREADMEを参照してください。

このコードベースで「〜のような仕様をモデル検査に通るまで実装して」というタスクを与えます。

https://github.com/miketako3/vibe-designing

形式手法の基礎知識

形式手法とは誤解を恐れずに言えばすごい自動テストです (詳しい方は怒らないでください)。

より数学的に厳密な方法で記述することで、その仕様を数学的に、機械的に検証できます。

TLA+

TLA+は形式手法の一種で、仕様記述用のプログラミング言語だと思ってもらえればだいたい大丈夫です。

TLA+は線形時相論理に基づいています。時相論理とは、よくある命題論理にある∀や∃に加えて□や◇を導入したものです。それぞれ以下を表しています。

□P: Pは今後常に真である
◇P: Pはいつか真になる

馴染みがないと意味不明だとは思いますが、なんとなく結果整合性とかを数学的に表せそうな雰囲気を感じてもらえればと思います。

要するにこのスーパー命題論理でシステムの仕様を記述すれば、厳密に矛盾が無いか数学的に評価できるということです。

以下はTLA+ (より正確にはTLA+にコンパイルされるPlusCal) で実装した仕様の例です。

-------------------------- MODULE Spec --------------------------
EXTENDS Integers, TLC

(*--algorithm Spec
variables
  flag = [i \in {1, 2} |-> FALSE];  \* 各プロセスの状態フラグ
  
process Proc \in {1, 2}
variables trying = FALSE;
begin
  ncs:  \* 非クリティカルセクション
    while TRUE do
      trying := TRUE;
      
  enter:  \* クリティカルセクションに入ろうとする
    flag[self] := TRUE;
    
  wait:  \* 他のプロセスが終わるのを待つ
    await ~flag[3 - self] \/ ~trying;
    
  cs:  \* クリティカルセクション
    skip;  \* クリティカルセクションでの処理
    
  exit:  \* クリティカルセクションを出る
    flag[self] := FALSE;
    trying := FALSE;
    
    goto ncs;  \* 非クリティカルセクションに戻る
  end while;
end process;

end algorithm; *)
\* BEGIN TRANSLATION (this part is generated by the TLA+ translator)
VARIABLES flag, pc, trying

vars == << flag, pc, trying >>

ProcSet == ({1, 2})

Init == (* Global variables *)
        /\ flag = [i \in {1, 2} |-> FALSE]
        (* Process Proc *)
        /\ trying = [self \in {1, 2} |-> FALSE]
        /\ pc = [self \in ProcSet |-> "ncs"]

ncs(self) == /\ pc[self] = "ncs"
             /\ trying' = [trying EXCEPT ![self] = TRUE]
             /\ pc' = [pc EXCEPT ![self] = "enter"]
             /\ flag' = flag

enter(self) == /\ pc[self] = "enter"
               /\ flag' = [flag EXCEPT ![self] = TRUE]
               /\ pc' = [pc EXCEPT ![self] = "wait"]
               /\ UNCHANGED trying

wait(self) == /\ pc[self] = "wait"
              /\ ~flag[3 - self] \/ ~trying[self]
              /\ pc' = [pc EXCEPT ![self] = "cs"]
              /\ UNCHANGED << flag, trying >>

cs(self) == /\ pc[self] = "cs"
            /\ TRUE
            /\ pc' = [pc EXCEPT ![self] = "exit"]
            /\ UNCHANGED << flag, trying >>

exit(self) == /\ pc[self] = "exit"
              /\ flag' = [flag EXCEPT ![self] = FALSE]
              /\ trying' = [trying EXCEPT ![self] = FALSE]
              /\ pc' = [pc EXCEPT ![self] = "ncs"]

Proc(self) == ncs(self) \/ enter(self) \/ wait(self) \/ cs(self)
                 \/ exit(self)

Next == (\E self \in {1, 2}: Proc(self))

Spec == Init /\ [][Next]_vars

\* END TRANSLATION
\* 安全性プロパティ: 2つのプロセスが同時にクリティカルセクションに入らない
MutualExclusion == ~(\E i, j \in {1, 2}: i # j /\ pc[i] = "cs" /\ pc[j] = "cs")

\* 活性プロパティ: プロセスがクリティカルセクションに入りたいとき、いつかは入れる
Liveness == \A self \in {1, 2}: (pc[self] = "wait" ~> pc[self] = "cs")
=============================================================================

なおこの仕様には穴があります。実際に検査してみると、2つのプロセスがお互いに待ち状態になってしまうデッドロックが検出されます。

モデル検査

モデル検査とは形式手法での検証方法の一つで、形式手法の言語で書かれたモデルに関して矛盾がないか検証することです。

イメージですが、ユーザーがN人でP個のサービスを使いそれぞれK個の状態があるとしたら、N×P×K個を全て検証します。実際に使う際にはN<5とかP<10とか制約を加えますが、それでも数万以上の状態を網羅的に検査できます。

先程の例示したTLA+のコードでも2つのプロセスが5つの動作をするパターンを網羅的に検証し、末尾に記載されたステータスをどんな状態でも必ず満たすことを確認できます。

全て検証しているのが重要で、その仕様においては数学的に記述した制約を常に満たすことが保証できます。熟練エンジニアが単に頑張ってやる設計とは次元が違う保証度合いです。

応用

特によく用いられるのは分散システムのアルゴリズムの検証です。AWSではS3に始まり、他のサービスでもTLA+がかなり積極的に用いられているようです。以下の記事が詳しいです。

https://masateruk.hatenablog.com/entry/2018/10/23/094048

直近でもこのような資料が公開されており、AWSで形式手法がかなり利用されているのがわかります。

https://queue.acm.org/detail.cfm?id=3712057

形式手法とVibe Coding

形式手法は前述の通り仕様に完全に矛盾がないかを検証できるため、大いにソフトウェア開発、特に設計において役に立つはずです。

一方で、形式手法は数学的な素養が必要で、コンピュータサイエンスの学位がないエンジニアが多い日本では普及が難しいのではないかと思っています。

ここで生成AIです。自然分で仕様を入力してVibe Codingで形式手法を用いて実装、それを検証できれば、特別な背景知識がなくても形式手法の恩恵を授かれるのではないかと考えました。

単に設計をmarkdownで書かせるのではなく形式手法を用いるのは、検証が付いてくるからです。出力された仕様が正しいかどうかは引き続き人間が確認する必要がありますが、少なくとも仕様自体に矛盾が無いかは自動で検証できるようになります。これは大きな差だと思います。

実行結果 ECサイトのポイント仕様

色々と試行錯誤してみたのですが、以下の仕様の指示は複雑すぎたのか構文チェックすら通らずでした。これでも現実の問題に比べたらかなりシンプルなのですが、まだ賢さが足らないようです。

また、全てを一気に出力するのも難しいようです。今回はECサイトのベースとポイント仕様、さらにはポイント上限という盛り盛りの仕様だったため、複雑過ぎたように思います。少しずつ仕様を追加していくのが良いでしょう。

指示

READMEを読み以下の仕様を作成し、エラーが無くなるまで仕様の追加と修正を加えてください
・ECサイトの購入のモデリング
・キャンペーンによるポイント付与
・ポイントは注文の変更に応じて最終的な付与額が変わる
・ポイントの付与は一定期間後
・ポイントには期間内に上限があり、超えてはならない
なお、実装はPlusCalのみで行ってください。TLA+の変換後のコードを直接弄ってはいけません (変換後に消えてしまうため)
また、.oldのファイルを見るとエラーがわかりやすいようです。変換に失敗した場合はそちらも参考にしてください

tlaファイル

EXTENDS Naturals, Sequences, FiniteSets, TLC

CONSTANT Customers, Products, MaxOrderItems, PointCap, GrantDelay, TimerId

ASSUME IsFiniteSet(Customers) /\ Customers /= {}
ASSUME IsFiniteSet(Products) /\ Products /= {}
ASSUME MaxOrderItems \in Nat \ {0}
ASSUME PointCap \in Nat \ {0}
ASSUME TimerId = {"timer"}
ASSUME GrantDelay \in Nat \ {0}

(*--algorithm ECPurchasePoints

variables
    orders = << >>,        \* Sequence of orders. Each order is a record:
                           \* [ customer \in Customers,
                           \*   items \in Seq(Products),
                           \*   status \in {"Pending", "Confirmed", "Cancelled", "Completed"},
                           \*   potential_points \in Nat,
                           \*   grant_timer \in 0..GrantDelay,
                           \*   final_points \in Nat ]
    customer_points = [c \in Customers |-> 0], \* Points per customer
    points_granted_this_period = [c \in Customers |-> 0] \* Points granted recently (for cap)

define
    \* Helper function to calculate points for an order based on a simple campaign (e.g., 1 point per item)
    CalculatePoints(items) == Len(items)

    \* Check if adding points exceeds the cap for a customer
    CanGrantPoints(customer, points_to_add) ==
        points_granted_this_period[customer] + points_to_add <= PointCap
end define;

process Customer \in Customers
variables my_order_index = -1, \* Index of the order this process instance is handling (0-based, -1 means no active order)
          state = "Start";     \* Local state machine: Start, Creating, Modifying, Waiting, Done
begin
MainLoop:
    while state /= "Done" do
        if state = "Start" then
            await Len(orders) < 10; \* Limit total orders for state space
            state := "Creating";

        elsif state = "Creating" then
            \* A customer creates an order
            with new_items = <<p>> \in {s \in Seq(Products) : Len(s) > 0 /\ Len(s) <= MaxOrderItems} do
                my_order_index := Len(orders); \* Index will be the current length (0-based)
                orders := Append(orders, [ customer |-> self,
                                           items |-> new_items,
                                           status |-> "Pending",
                                           potential_points |-> CalculatePoints(new_items),
                                           grant_timer |-> 0,
                                           final_points |-> 0 ]);
            end with;
            state := "Modifying";

        elsif state = "Modifying" then
ModifyChoice:
            either \* Customer confirms, modifies, or cancels the order
                ConfirmOrder: \* Re-added action label, removed branch label
\*                    assert orders[my_order_index].status = "Pending";
                    orders[my_order_index] := [orders[my_order_index] EXCEPT !.status = "Confirmed"];
                    orders[my_order_index] := [orders[my_order_index] EXCEPT !.grant_timer = GrantDelay]; \* Start the timer
                    state := "Waiting";
            or
                ModifyOrder: \* Re-added action label, removed branch label
\*                    assert orders[my_order_index].status = "Pending";
                        \* Drastically simplified for translator: do nothing in Modify branch for now
                        state := state; \* Dummy assignment to satisfy translator, state remains "Modifying"
            or
                CancelOrder: \* Re-added action label, removed branch label
\*                    assert orders[my_order_index].status = "Pending" \/ orders[my_order_index].status = "Confirmed";
                    orders[my_order_index] := [orders[my_order_index] EXCEPT !.status = "Cancelled",
                                                                            !.potential_points = 0,
                                                                            !.grant_timer = 0];
                    state := "Done"; \* Order cancelled
            end either;

        elsif state = "Waiting" then
            await orders[my_order_index].status = "Confirmed" /\ orders[my_order_index].grant_timer = 0;
            \* Timer finished, attempt to grant points
            with can_grant = CanGrantPoints(self, orders[my_order_index].potential_points) do skip; end with; \* Evaluate condition, do nothing else inside 'with'

            \* Labels re-added before if/else
                IfGrant:
                    if can_grant then
                        GrantAction:
                            orders[my_order_index] := [orders[my_order_index] EXCEPT !.final_points = orders[my_order_index].potential_points];
                        GrantPointsCust:
                        customer_points[self] := customer_points[self] + orders[my_order_index].final_points;
                    GrantPointsPeriod:
                        points_granted_this_period[self] := points_granted_this_period[self] + orders[my_order_index].final_points;
                    GrantPointsStatus:
                        orders[my_order_index] := [orders[my_order_index] EXCEPT !.status = "Completed"];
                ElseGrant:
                    else
                        NoGrantAction:
                            \* Point cap reached for this period, points not granted for this order
                            orders[my_order_index] := [orders[my_order_index] EXCEPT !.final_points = 0, !.status = "Completed"]; \* Mark as completed, but no points
                    orders[my_order_index] := [orders[my_order_index] EXCEPT !.final_points = 0, !.status = "Completed"]; \* Mark as completed, but no points
                end if;
            EndGrantCheck:
            state := "Done";

        else \* Should not happen, but ensures termination
            state := "Done";
        end if;
    end while;
    \* Process ends when state becomes "Done"
end process;

process TimerProcess = "timer"
begin
TickLoop:
    while TRUE do
        Tick: \* Label for the action within the loop
            \* Decrement grant timers for confirmed orders
        orders := [ i \in DOMAIN orders |->
                       LET order == orders[i] IN
                       IF order.status = "Confirmed" /\ order.grant_timer > 0 THEN
                           [order EXCEPT !.grant_timer = order.grant_timer - 1]
                       ELSE order
                   ];
        \* TODO: Add logic to reset points_granted_this_period periodically
    end while;
end process;

end algorithm; *)

cfgファイル

\* Define constants for the model checker
CONSTANT
    Customers = {c1, c2}
    Products = {p1, p2}
    MaxOrderItems = 2
    PointCap = 5
    GrantDelay = 2
    TimerId = {"timer"}

\* Specify the invariant to check
INVARIANT TypeInvariant
\* INVARIANT PointCapRespected \* Uncomment later
\* INVARIANT PointsOnlyForCompleted \* Uncomment later

\* Specify properties to check (optional)
\* PROPERTY PointsEventuallyGranted \* Uncomment later

\* Specify the initial state and next-state relation
INIT Init
NEXT Next

\* Optional: Symmetry definition if applicable
\* SYMMETRY PermutationsOfCustomers

properties.tlaファイル

EXTENDS ECPurchasePoints

\* Define the type invariant to ensure variables stay within their expected types.
TypeInvariant ==
    /\ \A c \in Customers : customer_points[c] \in Nat
    /\ \A c \in Customers : points_granted_this_period[c] \in Nat
    /\ orders \in Seq(SUBSET [ customer: Customers,
                               items: Seq(Products),
                               status: {"Pending", "Confirmed", "Cancelled", "Completed"},
                               potential_points: Nat,
                               grant_timer: 0..GrantDelay,
                               final_points: Nat ])
    /\ \A i \in DOMAIN orders : orders[i].potential_points = CalculatePoints(orders[i].items)
                                \/ orders[i].status = "Cancelled" \* Potential points are 0 if cancelled
    /\ \A i \in DOMAIN orders : orders[i].status /= "Completed" => orders[i].final_points = 0
    /\ \A i \in DOMAIN orders : orders[i].status = "Completed" => orders[i].final_points <= orders[i].potential_points
    /\ \A c \in Customers : points_granted_this_period[c] <= PointCap

\* Add other properties to check later, e.g., points are eventually granted if conditions met.
PointsEventuallyGranted(o_idx) ==
    LET order == orders[o_idx] IN
    (order.status = "Confirmed" /\ CanGrantPoints(order.customer, order.potential_points)) ~> (order.status = "Completed" /\ order.final_points = order.potential_points)

\* Points should not exceed the cap
PointCapRespected ==
    [](\A c \in Customers : points_granted_this_period[c] <= PointCap)

\* Points are only granted for completed orders
PointsOnlyForCompleted ==
    [](\A i \in DOMAIN orders : orders[i].final_points > 0 => orders[i].status = "Completed")

\* Total customer points should reflect granted points
CustomerPointsCorrect ==
    [](\A c \in Customers : customer_points[c] = Cardinality({i \in DOMAIN orders : orders[i].customer = c /\ orders[i].status = "Completed"}) * orders[i].final_points) \* Needs refinement if points vary

=============================================================================
\* Modification History
\* Last modified Wed Apr 09 16:01:35 JST 2025 by XXXXX

実行結果 ECサイトの注文仕様

ポイント仕様は全て削除し、ECサイトの注文状態の遷移に絞りました。

Rate Limitに入ってしまったので、結局Claudeと自分の手で結構編集しました。これは仕様としては簡単すぎますが、注文の状態の遷移に矛盾がないかを検証しています。これくらいであれば現状の生成AIでも作れそうですね。

Claudeにtlaファイルを渡して出力された状態遷移図がこちらです。

指示

READMEを読み以下の仕様を作成し、エラーが無くなるまで仕様の追加と修正を加えてください
・ECサイトの購入のモデリング
・注文の状態を用意し、違反な遷移がないことを確認
初回実装のためなるべくコード量を少なくシンプルに保ってください
なお、実装はPlusCalのみで行ってください。TLA+の変換後のコードを直接弄ってはいけません (変換後に消えてしまうため)
また、.oldのファイルを見るとエラーがわかりやすいようです。変換に失敗した場合は参考にしてください

tlaファイル

---- MODULE Spec ----
(*--algorithm purchase_process
process User = "User"
variables
    order_state = "cart";  (* 初期状態: カート *)
begin
UserAction:
    while order_state /= "shipped" /\ order_state /= "cancelled" do
        either
            \* カート → 注文済み
            await order_state = "cart";
            order_state := "ordered";
        or
            \* 注文済み → キャンセル済み
            await order_state = "ordered";
            order_state := "cancelled";
        or
            \* 支払い済み → キャンセル済み（返金処理）
            await order_state = "paid";
            order_state := "cancelled";
        end either;
    end while;
end process;

process System = "System"
begin
SystemAction:
    while order_state /= "shipped" /\ order_state /= "cancelled" do
        either
            \* 注文済み → 支払い済み（決済処理）
            await order_state = "ordered";
            order_state := "paid";
        or
            \* 支払い済み → 配送済み
            await order_state = "paid";
            order_state := "shipped";
        end either;
    end while;
end process;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "1f4e8047" /\ chksum(tla) = "c1bd906a")
VARIABLES pc, order_state

vars == << pc, order_state >>

ProcSet == {"User"} \cup {"System"}

Init == (* Process User *)
        /\ order_state = "cart"
        /\ pc = [self \in ProcSet |-> CASE self = "User" -> "UserAction"
                                        [] self = "System" -> "SystemAction"]

UserAction == /\ pc["User"] = "UserAction"
              /\ IF order_state /= "shipped" /\ order_state /= "cancelled"
                    THEN /\ \/ /\ order_state = "cart"
                               /\ order_state' = "ordered"
                            \/ /\ order_state = "ordered"
                               /\ order_state' = "cancelled"
                            \/ /\ order_state = "paid"
                               /\ order_state' = "cancelled"
                         /\ pc' = [pc EXCEPT !["User"] = "UserAction"]
                    ELSE /\ pc' = [pc EXCEPT !["User"] = "Done"]
                         /\ UNCHANGED order_state

User == UserAction

SystemAction == /\ pc["System"] = "SystemAction"
                /\ IF order_state /= "shipped" /\ order_state /= "cancelled"
                      THEN /\ \/ /\ order_state = "ordered"
                                 /\ order_state' = "paid"
                              \/ /\ order_state = "paid"
                                 /\ order_state' = "shipped"
                           /\ pc' = [pc EXCEPT !["System"] = "SystemAction"]
                      ELSE /\ pc' = [pc EXCEPT !["System"] = "Done"]
                           /\ UNCHANGED order_state

System == SystemAction

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == User \/ System
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION 
StateTypeOK ==  (* 状態の型チェック *)
  order_state \in {"cart", "ordered", "paid", "shipped", "cancelled"}

StateTransitionInvariant ==
  ~(order_state = "shipped" /\ order_state = "cancelled")

EventuallyShipped ==  (* 支払済注文は最終的に配送される *)
  order_state = "paid" => <>(order_state = "shipped")
=============================================================================

cfgファイル

\* Add statements after this line.
SPECIFICATION Spec
INVARIANT StateTypeOK
INVARIANT StateTransitionInvariant
PROPERTY EventuallyShipped
CHECK_DEADLOCK TRUE

properties.tlaファイル

StateTypeOK ==  (* 状態の型チェック *)
  order_state \in {"cart", "ordered", "paid", "shipped", "cancelled"}

StateTransitionInvariant ==
  ~(order_state = "shipped" /\ order_state = "cancelled")

EventuallyShipped ==  (* 支払済注文は最終的に配送される *)
  order_state = "paid" => <>(order_state = "shipped")

終わりに

結局現状の適当なVibe Codingでは簡単な仕様しか出力できないことがわかりました。

ただし逆に言えば、簡単な仕様においては矛盾のないことの保証付きで出力することができました。

コーディングをVibe Codingをする前に仕様をVibe Codingする、さらにはその仕様を形式手法で保証する。するとその仕様をコンテキストに入れてコーディング精度も上がるんじゃないかと考えます。

この記事の内容が全読者に伝わるとは思っていませんが、AIに投げるキーワードを知る機会になっていれば幸いに思います。