CUE、Quint、Apalache、Bazelを一本の依存グラフでつなぐ開発パイプラインのイラスト

Summary

この文書の要点

CUEは静的な正しさ、つまり「何が許されるか」の正本です。データ構造、設定、契約、制約、ポリシーをここに集約します。
Quintは動的な正しさ、つまり「どう遷移してよいか」の正本です。状態遷移、並行処理、冪等性、障害時の不変条件をモデル化します。
ApalacheはQuintモデルの検査バックエンドであり、実装の代わりではありません。`quint verify`から呼び出します。
Bazelは4つを別々の手順として走らせるのではなく、生成・検証・テストを一つの依存グラフで実行する基盤です。

1. 静的な契約だけでは、再実行と障害を止められない

CUEを正本にした型生成は、API、設定、権限、イベントの形を揃えるために必要です。一方で、同じ注文IDが二重に届く、決済の応答が途中で消える、確認と取消が同時に走る、といった問題は、型が正しくても起きます。

テストは具体例を示しますが、並行処理の組み合わせや、障害の挟まり方を数え上げる用途には向きません。コメントに「冪等にする」と書いても、再実行で残高が二度増える経路が残ることがあります。

そこで当社では、静的な契約と動的な振る舞いを別の正本に分け、両方を同じ変更の検証経路へ載せます。

CUEとBazelの型生成そのものは、別文書「CUEを正本とした型生成パイプラインとBazelによる堅牢・高速なビルド基盤」で扱っています。本稿は、その先にある状態遷移と障害時の不変条件までを、一つのパイプラインとして固定する話です。

静的な正本: フィールド、列挙、範囲、必須性、権限、許可された遷移表。CUEが担当します。
動的な正本: 初期状態、アクション、並行実行、再送、クラッシュ、不変条件。Quintが担当します。
検査: QuintモデルをApalacheで調べ、反例が出れば実装前に戻します。
実行: CUEの検証、Quintの検査、コード生成、テストをBazelの依存グラフで回します。

CUEを正本とした型生成パイプラインとBazelによる堅牢・高速なビルド基盤

2. 4つの役割は、置き換えではなく接続する

CUE、Quint、Apalache、Bazelは、互いに代わりになる道具ではありません。担当を分け、接続順を固定します。

CUEに状態機械の全経路を書こうとすると、制約言語の役割を超えます。QuintにOpenAPIや各言語の型を生成させようとすると、仕様言語の役割を超えます。Apalacheにコンテナを作らせることも、Bazelに業務上の不変条件を定義させることもしません。

接続の要点は、語彙を共有し、検査の順番を固定することです。注文状態の列挙はCUEを正とし、Quint側の状態集合と名前を一致させます。許可された遷移表もCUEに置き、Quintのアクションがその表を破らないことを不変条件にします。生成物や実装は、この二つの正本から下流へ流します。

CUE: データ構造、設定、契約、制約、ポリシー。時間を持たない正しさ。
Quint: 状態、アクション、並行性、冪等性、障害を含む実行の正しさ。
Apalache: QuintモデルをSMT制約へ落とし、指定した手数の範囲で不変条件を検査する。
Bazel: 上記の検証、生成、テスト、成果物化を、入力と依存関係から実行する。

3. CUE：データ構造、設定、契約、制約、ポリシー

CUEは、時間を持たない正しさの正本です。注文IDの形、金額の範囲、必須フィールド、権限、許可された遷移表のように、値がその瞬間に成立するかどうかをここに集めます。状態が「draft」から「paid」へ直接移ってよいかは遷移表としてCUEに置きますが、二重決済やクラッシュ後の再実行で残高がどうなるかはCUEの役割ではありません。

語彙の共有が、後段のQuintと生成物を同じ意味へ揃える条件です。状態の列挙名、金額の単位、注文IDの識別子はCUEを正とし、Quintの状態集合と生成される型へ同じ名前を渡します。CUE側で列挙を増やしたら、Quint側の状態と許可遷移も同じ変更として検証します。

`cue vet`は、設定やイベントの具体値が契約に合うかを先に確認します。検証を通った定義から型とスキーマを生成し、Quintモデルが参照する列挙と遷移表も同じ入力から揃えます。CUEに業務の全経路を書かせると、制約言語の役割を超えるため、時間を含む振る舞いはQuintへ渡します。

正本にする範囲: フィールド、列挙、範囲、必須性、権限、許可された遷移表。
Quintへ渡す語彙: 状態名、識別子、金額の意味。名前を一致させ、遷移表を破らないことを不変条件にする。
CUEに置かないもの: 再実行、並行処理、クラッシュを含む時間方向の経路。これはQuintが担当する。

CUEで注文・決済の契約と許可遷移を定義する例

#OrderStatus: "draft" | "confirmed" | "cancelled" | "paid"

#Order: {
  id:       string
  status:   #OrderStatus
  total:    number & >=0
  currency: *"JPY" | "JPY" | "USD"
}

#Payment: {
  orderId: string
  amount:  number & >=0
  attempt: int & >=1
}

#allowedTransitions: {
  draft:     ["confirmed", "cancelled"]
  confirmed: ["paid", "cancelled"]
  paid:      []
  cancelled: []
}

order: #Order & {
  id:     "order-001"
  status: "confirmed"
  total:  1200
}

4. Quint：状態遷移、並行処理、冪等性、障害時の不変条件

Quintは、どう遷移してよいかの正本です。初期状態、アクション、並行実行、再送、クラッシュ、不変条件をモデルにします。CUEの列挙と遷移表を前提にし、同じ注文IDが再度届いたとき残高が増えないこと、確認と取消が同時に走っても許可外の状態へ落ちないこと、応答が消えたあとの再実行で二重計上しないことを、コメントではなくモデルとして書きます。

テストは「この入力ならこうなる」を示します。Quintは、手数の範囲で取りうる経路を調べるための仕様です。決済モジュールでは、未処理の支払いだけが残高を増やし、処理済みIDの再送は状態を変えず、取消が先に確定すれば支払いを拒否する、といった規則をアクションと不変条件へ分けます。

モデルは実装の下書きではありません。画面の描画、HTTPの再試行実装、台帳の物理配置はQuintに書きません。業務上壊れてはいけない経路だけを残し、語彙はCUEと一致させます。モデルが膨らんだら、検査対象を狭く戻します。

Quintで決済モジュールの状態遷移と不変条件を定義する例

module payment {
  type Status = "draft" | "confirmed" | "paid" | "cancelled"

  var status: Status
  var balance: int
  var processed: Set[str]

  def allowed(from: Status, to: Status): bool = or {
    from == "draft" and to == "confirmed",
    from == "draft" and to == "cancelled",
    from == "confirmed" and to == "paid",
    from == "confirmed" and to == "cancelled",
  }

  action init = all {
    status' = "draft",
    balance' = 0,
    processed' = Set(),
  }

  action confirm = all {
    allowed(status, "confirmed"),
    status' = "confirmed",
    balance' = balance,
    processed' = processed,
  }

  action cancel = all {
    allowed(status, "cancelled"),
    status' = "cancelled",
    balance' = balance,
    processed' = processed,
  }

  action pay(id: str, amount: int): bool = all {
    allowed(status, "paid"),
    amount > 0,
    not(id.in(processed)),
    status' = "paid",
    balance' = balance + amount,
    processed' = processed.union(Set(id)),
  }

  action replay(id: str): bool = all {
    id.in(processed),
    status' = status,
    balance' = balance,
    processed' = processed,
  }

  val inv_balance_nonneg = balance >= 0
  val inv_paid_has_id = status != "paid" or processed.size() >= 1
  val inv_replay_keeps_balance = true
}

Quint公式ドキュメント

5. Apalache：実装の代わりではなく、モデルの検査バックエンド

Apalacheは、QuintモデルをSMT制約へ落とし、指定した手数の範囲で不変条件を検査します。実装の代わりではなく、`quint verify`から呼び出す検査バックエンドです。反例が出たら、コードを直す前にモデルか契約へ戻します。

`quint run`はランダムな実行で直感を確認し、`quint verify`はApalacheを使って手数の範囲を調べます。検証は全経路の証明ではありません。手数、状態空間、不変条件の置き方によって、見逃す経路が残ります。無限実行や livelock の完全な保証をApalacheに期待しません。

検査対象を増やしすぎると、時間だけが伸びてフィードバックが遅くなります。決済の冪等性、許可外遷移、障害後の再実行のように、壊れると金額や権限が崩れる条件から始めます。モデルが通っても実装が正しいとは限らないため、生成とテストは別ゲートとして残します。

ApalacheはQuintモデルを検査する。実装、コンテナ、型生成は担当しない。
手数の範囲で不変条件を調べ、反例が出れば実装前にモデルへ戻す。
全経路の証明ではなく、壊れてはいけない条件を先に固定する。

quint run と quint verify

quint run models/payment.qnt \
  --invariant=inv_balance_nonneg \
  --invariant=inv_paid_has_id \
  --max-samples=200

quint verify models/payment.qnt \
  --invariant=inv_balance_nonneg \
  --invariant=inv_paid_has_id \
  --max-steps=12

6. Bazel：生成・検証・テストを一つの依存グラフとして回す

Bazelは、CUE、Quint、Apalache、生成器、テストを別々の手順として走らせません。入力と依存関係から、検証、生成、テスト、成果物化を一つのグラフとして実行します。CUEが変われば`cue_vet`と生成が再実行され、遷移表が変わればQuintの検査が再実行され、生成物が変われば差分確認とテストが続きます。

カスタムルールの名前は組織ごとに違っても、役割は固定します。`cue_vet`は静的な契約、`quint_verify`は動的なモデル、`genrule`は型やスキーマの生成、`sh_test`は生成物の差分ゼロや契約テストです。Bazelに業務上の不変条件を書かせません。不変条件はQuintに置き、Bazelはその検査を依存ターゲットとして呼びます。

グラフが正確なら、変更された契約とモデル、その逆向き依存だけを実行できます。ローカルとCIで同じBUILD定義を共有し、キャッシュと並列実行でフィードバックを短くします。再現性は、入力、ツールチェーン、モデル、生成器の版を固定して初めて成り立ちます。

CUE: 契約と制約の検証。
Quint / Apalache: 状態遷移と不変条件の検査。
genrule: 型、スキーマ、コードの生成。
sh_test: 生成差分、契約テスト、障害時の適合確認。

Bazelターゲットの概念例

cue_vet(
    name = "contracts_vet",
    srcs = ["//contracts:order.cue"],
)

quint_verify(
    name = "payment_verify",
    srcs = ["//models:payment.qnt"],
    invariants = [
        "inv_balance_nonneg",
        "inv_paid_has_id",
    ],
    max_steps = 12,
)

genrule(
    name = "generate_types",
    srcs = ["//contracts:order.cue"],
    outs = [
        "order.go",
        "order.ts",
    ],
    cmd = "$(location //tools:cuegen) $< $(OUTS)",
    tools = ["//tools:cuegen"],
)

sh_test(
    name = "generated_diff_zero",
    srcs = ["check_generated.sh"],
    data = [
        ":generate_types",
        "//generated:all",
    ],
)

7. パイプラインの全体像

入口はCUEの契約です。列挙、制約、許可遷移を検証したあと、同じ語彙でQuintモデルを置きます。Apalacheは`quint verify`経由でそのモデルを検査し、反例があれば生成より前に戻します。通った契約から型とコードを生成し、Bazelが検証・生成・テストを依存グラフとして回します。

品質ゲートでは、生成物を直接編集していないこと、契約テストと冪等性の適合テストが通ること、成果物が依存グラフから作られることを確認します。運用で見つかった実装差異は、個別実装へ閉じるか、CUEかQuintの正本へ戻すかを分けます。この戻り道がないと、現場の例外がコメントとテストに散らばります。

CUE: 何が許されるかを定義する。
Quint: どう遷移してよいかを定義する。
Apalache: 指定手数の範囲で不変条件を検査する。
生成とBazel: 正本から派生成果物を作り、依存グラフで実行する。
ゲート: 生成差分、契約適合、成果物の成立性を確認する。

CUEからQuint・Apalache・生成・Bazel・品質ゲートへ進む流れ

flowchart LR
  subgraph CUE["CUE：静的な正本"]
    ST["構造・契約・制約・ポリシー"]
  end
  subgraph QNT["Quint：動的な正本"]
    MD["状態遷移・不変条件"]
  end
  subgraph APA["Apalache：検査"]
    VF["quint verify"]
  end
  subgraph GEN["生成"]
    CG["型・スキーマ・コード"]
  end
  subgraph BZL["Bazel：依存グラフ"]
    TG["検証・生成・テスト target"]
  end
  subgraph GATE["品質ゲート"]
    DF["生成差分ゼロ / 契約テスト"]
  end
  subgraph OUT["成果物"]
    AR["バイナリ・コンテナ"]
  end
  ST --> MD --> VF
  ST --> CG
  VF --> TG
  CG --> TG
  TG --> DF --> AR

8. CIで検証を段階化する

CIでは、いきなり全サービスをビルドしません。静的な契約、動的なモデル、生成の再現性、実装の適合、成果物の成立を段階に分けます。早い段階で失敗させれば、コンテナのログを読む前に、原因をCUEかQuintへ戻せます。

第一段階でCUEを検証し、第二段階でQuintの構文確認と`quint run`によるシミュレーションを行います。第三段階でApalacheによる不変条件検査を走らせ、反例があれば生成へ進みません。第四段階でスキーマとコードを生成し、第五段階でGit管理対象の生成物に差分がないことを確認します。

第六段階以降はBazelで静的解析と差分テストを実行します。第七段階では、APIの入出力だけでなく、冪等性、再実行、障害復旧のように型だけでは保証できない適合条件をテストします。最後にバイナリとコンテナを生成します。生成物をGitへ含めない運用でも、同じ入力から同じ出力になることを検証します。

1. CUE構文・型・制約の検証
2. Quintモデルの構文確認とシミュレーション
3. Apalacheによる不変条件検査
4. CUEからのスキーマ・コード生成
5. 再生成後の差分ゼロ確認
6. Bazelによる静的解析と差分テスト
7. 契約・冪等性・障害復旧の適合テスト
8. バイナリ・コンテナの生成

生成物を直接編集していないことを確認する例

bazel test //contracts:contracts_vet //models:payment_verify
bazel run //contracts:generate_all
git diff --exit-code -- generated/ \
  || { echo "生成物はCUEから再生成してください"; exit 1; }

bazel test //contracts/changed:all \
  --test_output=errors

9. モデル化の範囲を狭く保つ

形式検証の失敗は、道具不足より範囲の取りすぎで起きます。画面遷移、HTTPの全ヘッダ、台帳の物理配置、すべての列挙値までQuintに書くと、モデルが実装の写しになり、検査時間が伸びて保守されなくなります。当社では、壊れると金額、権限、重複実行が崩れる経路だけをモデル化します。

対象にするのは、許可された遷移、冪等な再送、確認と取消の並行、応答消失後の再実行、クラッシュ直後の不変条件です。対象にしないのは、UIの見た目、ログの文面、インデックスの選び方、再試行のバックオフ実装、生成された型の細目です。細目はCUEと実装側へ残します。

モデルは「今の実装を説明するもの」ではなく、「実装が破ってはいけない条件」です。実装差異が見つかったとき、それが業務上の例外ならQuintへ昇格し、特定サービスの都合なら実装側へ閉じます。すべてをモデルに戻すと、正本が肥大します。

モデル化する: 許可遷移、冪等な再送、並行する確認と取消、障害後の再実行、残高や権限の不変条件。
モデル化しない: UI、通信の細部、永続化の最適化、生成型の形式固有の都合。
昇格の判断: 複数サービスが共有する壊れ方だけを正本へ戻す。

10. AIエージェント開発との相性

AIエージェントが実装を増やす環境では、生成量より、変更を同じ契約と検証規則へ収束させることが重要です。AIに自由に状態機械や再試行を設計させるのではなく、CUEの語彙、Quintのアクション、Bazelの許可された依存方向に従わせます。

AIが書いたコードは、`cue_vet`、`quint verify`、再生成差分ゼロ、静的解析、契約テスト、冪等性の適合テストを通します。生成物を直接書き換えた場合は、差分ゼロの検査で検出します。失敗時には、どのCUE契約、どのQuint不変条件、どのBazelターゲットが壊れたのかをラベルで示し、再試行の範囲を指定します。

並列エージェントが別サービスを変更する場合も、共通の静的正本と動的正本へ収束させます。例外を各実装へ増やすのではなく、契約変更ならCUEへ、振る舞い変更ならQuintへ、実装固有ならサービス境界へ戻します。自由度を制約することは速度を落とすためではなく、人が後から整合性を確認する範囲を小さくするための設計です。

AIに任せる範囲: 契約とモデルに従った実装、テスト、局所的な修正。
人が判断する範囲: 遷移の意味、互換性、認可、例外を正本へ昇格させるかどうか。
機械的なゲート: cue vet、quint verify、再生成差分、依存方向、契約・適合テスト。

11. 自社での採用方針

自社では、CUEをデータ構造、設定、契約、制約、ポリシーの正本とします。許可された遷移表もCUEに置き、Quintの状態集合と名前を一致させます。Protocol Buffers、OpenAPI、JSON Schema、各言語の型は、CUEから導出される派生成果物です。

Quintは、状態遷移、並行処理、冪等性、障害時の不変条件の正本とします。Apalacheは`quint verify`のバックエンドとして使い、実装や成果物の生成には使いません。検査手数と不変条件は、金額、権限、重複実行のように壊れてはいけない条件から固定します。

Bazelは、CUEの検証、Quintの検査、コード生成、適合テスト、バイナリとコンテナの生成をターゲット化し、変更された範囲だけを実行できる依存グラフへまとめます。生成物は原則として手動編集しません。変更はCUEまたはQuintから行い、生成差分と検査結果をCIで確認します。

この方針は、将来的なAIエージェントによる並列開発にも対応します。複数のエージェントが同時に実装しても、静的な契約と動的な振る舞いの二つの正本、そしてBazelのビルド規則へ変更を収束させます。

CUE: 構造、契約、制約、ポリシー、許可された遷移表。
Quint: 状態遷移、並行、再送、クラッシュ、不変条件。
Apalache: Quintモデルの検査。実装の代わりではない。
Bazel: 検証、生成、テスト、成果物化を一つの依存グラフで実行する。

12. まとめ：静的な契約と動的な振る舞いを一本の経路へ置く

型と設定が揃っていても、再実行、並行処理、途中障害で壊れる振る舞いは残ります。CUEで何が許されるかを定義し、Quintでどう遷移してよいかを定義し、Apalacheでそのモデルを検査し、Bazelで生成・検証・テストを一つの依存グラフとして回す。これが当社の開発標準です。

4つの道具は互いに代わりになりません。CUEに全経路を書かせず、Quintに型を生成させず、Apalacheにコンテナを作らせず、Bazelに業務上の不変条件を定義させません。語彙を共有し、検査の順番を固定し、生成物と実装を下流へ流します。

冪等性と障害時の不変条件は、コメントや後段テストだけに残しません。モデル化の範囲は狭く保ち、壊れると金額や権限が崩れる経路から検査します。宣言を正本にし、検査を依存グラフへ載せ、変更を同じ経路でマージまで届ける。この区別を保てるなら、CUE・Quint・Apalache・Bazelの組み合わせは、単なるツール選定ではなく、静的な契約と動的な振る舞いを一つの開発標準へ固定する設計になります。

CUE・Quint・Apalache・Bazelを一つのパイプラインにした開発標準