🍣
信頼性の高い設計を形式手法のTLA+とVibe Codingで作成しようとしてみた
概要
この記事ではTLA+を使ったテンプレートを作成し、その上でRoo CodeにVibe Codingさせることで、信頼性の高いビジネスロジックの設計を行おうと試みました。
モデルはgemini-2.5-pro-exp-03-25を用いました (お財布に優しい！)。
結果として、残念ながら実用的な複雑度を持った仕様はとても得られませんでした。ただし、簡単な仕様であれば、TLA+を用いたモデル検査を経た堅牢な状態を得ることができました。
今回用いたコード
これが欲しい人が多いと思いますので先んじて貼っておきます。指定のファイルに仕様を記述してスクリプトを実行すると、その仕様に矛盾がないかを検証できます。詳細な使い方はREADMEを参照してください。
このコードベースで「〜のような仕様をモデル検査に通るまで実装して」というタスクを与えます。
形式手法の基礎知識
形式手法とは誤解を恐れずに言えばすごい自動テストです (詳しい方は怒らないでください)。
より数学的に厳密な方法で記述することで、その仕様を数学的に、機械的に検証できます。
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+がかなり積極的に用いられているようです。以下の記事が詳しいです。
直近でもこのような資料が公開されており、AWSで形式手法がかなり利用されているのがわかります。
形式手法と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に投げるキーワードを知る機会になっていれば幸いに思います。
Discussion