はじめに

AIに頼めば、AlloyやTLA+やLeanのモデルは数分で出てくる。 書くのが速くなると、今度は別の心配が出てくる。 仕様を変えたとき、増えたモデルや証明のどれかが黙って古くなるのではないか。

そこで、同じ小さな承認フローを7つの道具で書き、わざと1か所だけ壊してみた。 壊し方はすべて同じで、「取消したのにアクセスを許す」にする。 道具が気づくか、気づいたらCIを止める終了コードを返すかを見る。 仕様と実装の対応を管理するdspecだけは役目が違うので、実装参照の名前を壊して別に試した。

結果は、7つのうちTLA+・Quint・Dafnyの3つがそのまま止まった。 LeanとCedarは、命題の書き方とテストの有無で結果が変わった。 AlloyとZ3は気づいたが、終了コードではCIを止めなかった。

題材：取消した依頼は許可しない

• 依頼はPendingから始まる
• approveするとApprovedになり、アクセスを許可する
• cancelするとCancelledになり、アクセスを許可しない
• Cancelledの依頼は、何をしても許可しない

題材は記事用に作った最小の例である。 7つのサンプルと壊した版はscripts/formal_methods_approval_2026にある。 壊した版はbroken/の下にあり、元の版との差は1行だけである。

壊した仕様に誰が気づいたか

止まらなかった道具には、それぞれ止める方法があった。

Leanは、書いた命題の外を見逃した。 元の定理は「取消済みの状態から先では許可しない」で、壊したpendingからcancelする行は範囲の外にある。 定理を「どの状態からでも、結果が取消済みなら許可しない」に強めると止まった。

Cedarは、期待値が無いと正誤を決めない。 authorizeは壊したポリシーでもALLOWと答えるだけで、期待値を書いたテストをrun-testsで流すと止まった。

AlloyとZ3は、終了コードを見るだけでは足りない。 どちらも違反を見つけても終了コード0で終わる。 CIで使うなら、違反を問う検査の結果を期待値と比べる処理を足す。 Alloyなら対象のcheckがUNSATか、Z3なら違反を問うcheck-satがunsatかを見る。 出力のどこかにsatが出たら落とす、という雑な判定では、正常な版も落ちる。

8つの道具は何を検査するか

Z3は、AlloyやTLA+と同じ意味の仕様言語ではない。 Dafnyをはじめ多くの検証器の下で働く推論エンジンで、業務の仕様をどう式にするかは使う側が決める。

Cedarは検証専用のモデルでもない。 同じポリシーを、Rust製のエンジンやAmazon Verified Permissionsが本番の認可判断に使う。

dspecは定理証明器でもモデル検査器でもない。 Pklの型付きモデルを正本にして、規則とAlloy・TLA+・Lean・テストなどの生成物、実装のどの関数がどの規則に対応するか（実装参照）を結び付ける。 正本から生成物を作ることを、dspecは射影と呼ぶ。

サンプルと、壊したときの出力

Alloy 6：有限の範囲で反例を探す

enum Status { Pending, Approved, Cancelled }
enum Grant { Denied, Granted }

sig User {}

sig Request {
  owner: one User,
  approver: one User,
  status: one Status,
  grant: one Grant
}

fact DistinctRoles {
  all r: Request | r.owner != r.approver
}

fact GrantMatchesStatus {
  all r: Request | r.grant = Granted iff r.status = Approved
}

assert CancelledNeverGrants {
  all r: Request | r.status = Cancelled implies r.grant = Denied
}

check CancelledNeverGrants for 4

java -jar alloy.jar exec -c CancelledNeverGrants -t json -o out approval.als

00. check CancelledNeverGrants     0       UNSAT

UNSATは、スコープ4の範囲でassertを破る構造が見つからなかったという意味である。 無限の範囲で証明したわけではない。

壊した版はGrantMatchesStatusをr.status != Pendingにした。 結果はSATになり、取消済みで許可された依頼が反例として出る。 終了コードは0のままだった。

TLA+ / TLC：すべての到達状態を調べる

---- MODULE Approval ----
VARIABLES status, granted

vars == <<status, granted>>

Init ==
  /\ status = "pending"
  /\ granted = FALSE

Approve ==
  /\ status = "pending"
  /\ status' = "approved"
  /\ granted' = TRUE

Cancel ==
  /\ status = "pending"
  /\ status' = "cancelled"
  /\ granted' = FALSE

Finish ==
  /\ status \in {"approved", "cancelled"}
  /\ UNCHANGED vars

Next == Approve \/ Cancel \/ Finish
Spec == Init /\ [][Next]_vars

CancelledNeverGrants == status = "cancelled" => ~granted
====

java -cp tla2tools.jar tlc2.TLC -config Approval.cfg Approval.tla

Model checking completed. No error has been found.
5 states generated, 3 distinct states found, 0 states left on queue.

終わった後の足踏みはFinishとして明示した。

Cancelのgranted'をTRUEにすると、TLCは取消1回の反例（初期状態と取消後の2状態）を出して終了コード12で止まる。

State 1: <Initial predicate>
/\ granted = FALSE
/\ status = "pending"

State 2: <Cancel line 16, col 3 to line 18, col 20 of module Approval>
/\ granted = TRUE
/\ status = "cancelled"

Quint：型付きの状態モデルをTLCで検査する

module approval {
  type Status = Pending | Approved | Cancelled

  var status: Status
  var granted: bool

  action init = all {
    status' = Pending,
    granted' = false,
  }

  action approve = all {
    status == Pending,
    status' = Approved,
    granted' = true,
  }

  action cancel = all {
    status == Pending,
    status' = Cancelled,
    granted' = false,
  }

  action step = any { approve, cancel }
  val cancelledNeverGrants = status != Cancelled or not(granted)
}

npx @informalsystems/quint@0.33.1 verify approval.qnt \
  --backend=tlc --invariant=cancelledNeverGrants --max-steps=5

[ok] No violation found (300ms).

cancelのgranted'をtrueにすると、[violation] Found an issueと反例を出して終了コード1で止まる。 TLCのバックエンドはJava 21以上が要る。Java 17では起動の段階で失敗した。

Quintは、モデルが作った実行の列を実装にも流して振る舞いを比べる、モデルベーステストにもつながる。 Quint Connectは、QuintのトレースをRustの実装へ再生する。

Dafny：契約つきの関数を証明する

datatype Status = Pending | Approved | Cancelled

method Approve(status: Status) returns (next: Status, granted: bool)
  requires status == Pending
  ensures next == Approved
  ensures granted
{
  next, granted := Approved, true;
}

method Cancel(status: Status) returns (next: Status, granted: bool)
  requires status == Pending
  ensures next == Cancelled
  ensures !granted
{
  next, granted := Cancelled, false;
}

dafny verify approval.dfy

Dafny program verifier finished with 3 verified, 0 errors

Cancelの本体をgranted := trueにすると、すぐ上のensures !grantedを証明できずに止まる（終了コード4）。

approval.dfy(15,0): Error: a postcondition could not be proved on this return path
Dafny program verifier finished with 2 verified, 1 error

Dafnyは契約と実装を同じ場所に書くので、実装を変えれば契約とぶつかる。 ただし証明できるのはDafnyで書いたコードである。 同じロジックを別にTypeScriptで手書きしていれば、そちらは証明の外にある。

Lean 4：命題が狭いと見逃す

def step : Status -> Event -> Status × Bool
  | .pending, .approve => (.approved, true)
  | .pending, .cancel => (.cancelled, false)
  | status, _ => (status, false)

-- 元の定理: 取消済みの状態から先では許可しない
theorem cancelledNeverGrants (event : Event) :
    (step .cancelled event).2 = false := by
  cases event <;> rfl

-- 強めた定理: どの状態からどの操作をしても、結果が取消済みなら許可しない
theorem cancelledResultNeverGrants (status : Status) (event : Event) :
    (step status event).1 = .cancelled → (step status event).2 = false := by
  cases status <;> cases event <;> decide

lean --run Approval.lean

status=Status.cancelled, granted=false

元の定理だけの版（broken/ApprovalOriginalTheorem.lean）で.pending, .cancelを(.cancelled, true)にすると、ファイルはそのまま受理される。 実行するとstatus=Status.cancelled, granted=trueが出る。 元の定理はstep .cancelled event、つまり取消済みの状態を入力にした遷移しか見ていないからだ。

強めた定理を入れた版では、同じ1行の変更で止まる（終了コード1）。

Approval.lean:24:35: error: Tactic `decide` proved that the proposition
  (step Status.pending Event.cancel).fst = Status.cancelled → (step Status.pending Event.cancel).snd = false
is false

元の定理の名前はcancelledNeverGrantsで、読むと正しそうに見える。 レビューで見るべきは定理の名前ではなく、量化している範囲である。

Z3：違反を直接聞く

(set-logic ALL)

(declare-datatypes () ((Status Pending Approved Cancelled)))
(declare-const before Status)
(declare-const after Status)
(declare-const granted Bool)

(assert (= before Pending))
(assert
  (or
    (and (= after Approved) (= granted true))
    (and (= after Cancelled) (= granted false))))

(push)
(assert (= after Cancelled))
(assert granted)
(check-sat)
(pop)

(check-sat)
(get-model)

unsat
sat

最初のunsatは「取消済みなのに許可」という状態が遷移と両立しないことを示す。 壊した版では、最初の答えがsatになる。 どちらの版でもZ3の終了コードは0なので、期待する答えと比べる処理を自分で書く。

Cedar：本番と同じポリシーを評価する

permit (
  principal == User::"approver",
  action == Action::"approve",
  resource is Request
);

permit (
  principal,
  action == Action::"read",
  resource is Request
) when {
  resource.status == "approved"
};

forbid (
  principal,
  action == Action::"read",
  resource is Request
) when {
  resource.status == "cancelled"
};

取消済みの依頼に対するreadはDENY（一致したのは3つめのforbid）、approverによるapproveはALLOWになる。

cedar authorize --policies approval.cedar --entities entities.json \
  --principal 'User::"approver"' --action 'Action::"read"' \
  --resource 'Request::"request-1"'

3つめのforbidをpermitにすると、authorizeはALLOWを返して終了コード0で終わる。 期待値を書いたテストのJSONをrun-testsに渡すと、壊した版で止まる。

cedar run-tests --policies approval.cedar --tests approval.cedar-tests.json

running 2 test(s)
  test cancelled request cannot be read ... fail: expected Deny, got Allow
  test approver can approve ... ok
results: 1 passed, 1 failed

Cedar自体の正しさは、Leanのモデル、Rustの実装、両者を比べるテストで支えられている。 それでも、業務の要件どおりのポリシーを書くことと、正しい主体・資源・文脈をCedarへ渡すことは、使う側の仕事として残る。

dspec：規則と実装の対応が切れたら止める

dspecには承認操作の決定表をPklで書いたfixtureがある。 上長のallowより、優先度の高いdenyの例外が勝つという決定だ。

new d.IntentAccessPolicy {
  id = "request.approve-manager-allow"
  process = "request.approve"
  subject = "role.manager"
  decision = "allow"
  priority = 100
}

new d.IntentAccessPolicy {
  id = "request.approve-manager-deny-exception"
  process = "request.approve"
  subject = "role.manager"
  decision = "deny"
  priority = 200
  overrides {
    "request.approve-manager-allow"
  }
}

node src/cli.mjs intent access --json fixtures/intent-contract.pkl \
  request.approve role.manager

{
  "decision": "deny",
  "policy": {
    "id": "request.approve-manager-deny-exception",
    "overrides": ["request.approve-manager-allow"],
    "priority": 200
  },
  "status": "pass"
}

dspec自身の正本にcheckとdriftをかけると、規則81、用語138、射影7、実装参照1,124件で両方ともpassになった。 正本にある実装参照loadModelを、存在しないloadModel_missing_for_testに書き換えると、driftが止まる（終了コード1）。

missing implementation symbol: DSPEC-TOPLEVEL-MODEL -> src/cli.mjs#loadModel_missing_for_test

dspecが見ているのは、規則に対応する関数がまだ存在するかである。 関数の中身が規則どおりかまでは見ない。 dspecのREADMEも、driftの役目を、実装参照がファイルやシンボルに今も解決できるかの検査としている。 検証の強さは、解決できるだけのreferenceと、executed・bounded・provedを分けて記録する。

ずれを抑える4つの設計

仕様を変えたときに古くなる成果物を減らす方法は、今のところ4つに分かれる。

今回の結果をこの表に重ねると、どの設計にも「書いていない命題は守られない」という穴が残る。 Leanの狭い定理と、期待値を書かないCedarは、同じ穴に落ちた例である。

どれを選ぶか

権限の組み合わせが複雑なとき。 設計段階でrole、tenant、所有、委任の矛盾を探すならAlloyが合う。 本番の認可まで同じ成果物で持ちたいならCedarを使い、期待値のテストをrun-testsでCIに入れる。

取消、タイムアウト、再試行が絡むとき。 TLA+かQuintを使う。 「取消の後に遅れて承認が届く」のような順序の問題は、決定表では書きにくい。 Quintは型と実行とテストに寄せたいとき、TLA+は既存の事例やTLAPSでの証明まで使いたいときに向く。

関数そのものを証明したいとき。 Dafnyは自動証明の比重が高く、契約とコードを一緒に書ける。 Leanは命題と証明の書き方を細かく制御できる。 どちらも、定理が何を量化しているかをレビューで確かめる。

成果物が増えてきたとき。 dspecのように、規則・実装参照・生成物・検証結果を1つの型付きモデルに戻すと、参照の切れはCIで止められる。 意味の一致までは保証しないので、上の検証器やテストと組み合わせる。

実行した版

出典

• Alloy: Alloy applications、case studies
• TLA+: Leslie LamportのTLA+のページ、Use of Formal Methods at Amazon Web Services
• Quint: Quintのドキュメント、use cases
• Dafny: Dafny reference、AWSでの利用
• Lean 4: Lean language reference、Mathlib
• Z3: Z3: an efficient SMT solver
• Cedar: Cedar security model、Amazon Verified Permissions
• dspec: mizchi/dspec、Apple Pkl
• 分類: 三菱総合研究所「形式手法・ツール分類」

おわりに

同じ1行の壊し方に対して、止まった道具と素通りした道具があった。 差を生んだのは道具の強さより、命題をどこまで広く書いたか、期待値をテストに書いたか、CIが終了コードと出力のどちらを見るかだった。

AIでモデルを増やすなら、モデルと一緒に「壊したら落ちるか」も確かめておきたい。 壊した版は1行で作れて、CIで毎回流せる。