Quintで始めるモデルベーステスト: 仕様のコード化とHono向け結合テストの作り方

仕様書からテストケースを作成する際、テキストからコードの変換作業は開発者のスキルに依存しがちです。そのため、仕様に対してテストケースが十分であるかなどの確認部分に抜け穴などが生まれがちでした。これは生成AIによるテスト作成などでも同様で、「仕様がテストにどれだけ落とし込まれているか」をコードなどで表現します。

本記事では、在庫予約APIを題材に、Quintで検査した仕様からテストの期待値を取り出し、vitestでHono実装に流し込んで確かめる方法を示します。

本記事のコマンドとコードは、2026-10-01に実行して確認したものです。確認環境は@informalsystems/quint 0.33.0、hono 4.13.12、vitest 5.0.3、create-hono 0.19.5のcloudflare-workersテンプレート、Node.js 22.22.2です。

Quintとは？

Quintは、Leslie LamportのTLA（Temporal Logic of Actions）を理論的な土台とする仕様記述言語です。書いた仕様はシミュレータで実際に動かせます。

仕様を書く目的は2つあります。1つは、実装より先に「設計そのものが壊れていないか」を機械に探させることです。在庫が負になる、在庫と予約の合計が合わなくなる、といった性質違反を、シミュレータが反例として見つけます。もう1つは、検査済みの仕様を「正解の振る舞い」としてテストに使うことです。これがモデルベーステスト（MBT）で、本記事の後半で扱う内容です。

ここから、仕様を書き、仕様を検査し、仕様からトレースを出して読み方を知り、そのトレースを使うテストを実装より先に書きます。テストの失敗に導かれてHono実装を少しずつ書き、実装のバグが検出されることを確かめました。仕様を正解としたTDDです。

プロジェクトを用意する

Hono公式のcreate-honoで、Cloudflare Workers向けのテンプレートから始めます。

npm create hono@latest hono-quint
#  Which template do you want to use? → cloudflare-workers
#  Do you want to install project dependencies? → Yes
#  Which package manager do you want to use? → npm

cd hono-quint
npm i -D @informalsystems/quint vitest
npx quint --version   # 0.33.0

テンプレートのsrc/index.tsは、new Hono()で作ったアプリをそのままexport defaultしています。テストのたびに真っさらな状態のアプリを作れるよう、アプリの生成をcreateApp(initialStock)という独立した関数にし、src/app.tsに移しました。

テストはCloudflare Workersのランタイムではなく、通常のvitest（Node.js上）で実行します。テストがnode:child_processでquintを呼び、node:fsでトレースを読むためです。

仕様を書く

APIが守るべき決まりを先に整理します。初期在庫は3です。

エンドポイント	条件	ステータスコード
POST /reservations	在庫が残っている	201（予約を作成）
POST /reservations	在庫切れ	409
DELETE /reservations/:id	予約が存在する	204（在庫を戻す）
DELETE /reservations/:id	予約が存在しない	404

この決まりをQuintで書いたものがspec/reservation.qntです。

module reservation {
  // テストが API に送るリクエストを、仕様の中で値として表す
  type Request =
    | Start                // 初期状態（リクエストなし）
    | Reserve(str)         // POST /reservations { user }
    | Cancel(int)          // DELETE /reservations/:id

  pure val INITIAL_STOCK = 3
  pure val USERS = Set("alice", "bob")
  pure val IDS = 1.to(5)

  // ---------- 状態 ----------
  var stock: int                  // 残り在庫数
  var reservations: int -> str    // 予約ID -> ユーザー
  var nextId: int                 // 次に払い出す予約ID
  var lastRequest: Request        // 直前に受けたリクエスト
  var lastStatus: int             // そのリクエストに返すべきステータスコード

  action init = all {
    stock' = INITIAL_STOCK,
    reservations' = Map(),
    nextId' = 1,
    lastRequest' = Start,
    lastStatus' = 0,
  }

  // POST /reservations：在庫があれば201、なければ409
  action reserve(user: str): bool = all {
    lastRequest' = Reserve(user),
    if (stock > 0) all {
      stock' = stock - 1,
      reservations' = reservations.put(nextId, user),
      nextId' = nextId + 1,
      lastStatus' = 201,
    } else all {
      stock' = stock,
      reservations' = reservations,
      nextId' = nextId,
      lastStatus' = 409,
    },
  }

  // DELETE /reservations/:id：存在すれば在庫を戻して204、なければ404
  action cancel(id: int): bool = all {
    lastRequest' = Cancel(id),
    if (reservations.keys().contains(id)) all {
      stock' = stock + 1,
      reservations' = reservations.keys().exclude(Set(id)).mapBy(k => reservations.get(k)),
      nextId' = nextId,
      lastStatus' = 204,
    } else all {
      stock' = stock,
      reservations' = reservations,
      nextId' = nextId,
      lastStatus' = 404,
    },
  }

  // 環境：どのリクエストがいつ来るか
  action step = {
    nondet user = USERS.oneOf()
    nondet id = IDS.oneOf()
    any {
      reserve(user),
      cancel(id),
    }
  }

  // 不変条件：どの状態でも成り立つべき性質
  val stockNeverNegative = stock >= 0
  val stockIsConserved = stock + reservations.keys().size() == INITIAL_STOCK

  run soldOutTest =
    init
      .then(reserve("alice"))
      .then(reserve("bob"))
      .then(reserve("alice"))
      .then(reserve("bob"))
      .expect(lastStatus == 409 and stock == 0)

  run cancelRestoresStockTest =
    init
      .then(reserve("alice"))
      .then(cancel(1))
      .expect(lastStatus == 204 and stock == INITIAL_STOCK)

  run cancelUnknownIdTest =
    init
      .then(cancel(1))
      .expect(lastStatus == 404 and stock == INITIAL_STOCK)
}

lastRequestとlastStatusは、テストのために用意した状態です。トレースを読むだけで「何を送り、何が返るべきか」が分かるようにしています。actionは状態を一歩進める規則で、stepは外の世界からどんなリクエストが来うるかを表します。stockNeverNegativeとstockIsConservedが不変条件で、どの状態でも成り立つべき性質です。

仕様を検査する

型検査を通してから、シミュレータで不変条件が破れていないかを確かめます。

npx quint typecheck spec/reservation.qnt  # 型とeffectを検査
npx quint run spec/reservation.qnt --backend typescript \
  --invariants stockNeverNegative stockIsConserved --max-steps 30  # 不変条件をシミュレータで検査

--backend typescriptを指定しています。Quint 0.33.0のquint runとquint testは、既定のバックエンドがrustです（npx quint run --helpで確認）。Rustバックエンドは初回実行時にGitHubから取得されますが、確認環境では取得できなかったため、--backend typescriptで動かしました。

次に、仕様へわざと誤りを入れて、検査の出力を見ます。

箇所	変更前	変更後
reserveの条件	stock > 0	stock >= 0

この書き換えで、在庫0のときも予約できてしまう設計になります。

npx quint run spec/reservation.qnt --backend typescript \
  --invariants stockNeverNegative stockIsConserved --max-steps 30  # 誤りを入れた仕様を再検査

在庫が-1になる状態までの実行例が、反例として示されます。

[State 5]
{ lastRequest: Reserve("alice"), lastStatus: 201, nextId: 5, reservations: Map(1 -> "alice", 2 -> "alice", 3 -> "alice", 4 -> "alice"), stock: -1 }

[violation] Found an issue (11ms at 91 traces/second).
  ❌ stockNeverNegative

実装を一行も書く前に、設計上の穴がこの形で見つかりました。確認したらgit checkout spec/reservation.qntで元に戻してください。

仕様そのものにテストを書く

不変条件は「どの状態でも成り立つ性質」でした。それとは別に、「この順番で操作したらこうなるはず」という具体例も仕様側で確かめられます。仕様末尾のrunがそれです。init.then(reserve("alice"))...のように操作を順に並べ、.expect(...)で最後の状態を検査する流れです。

npx quint test spec/reservation.qnt --backend typescript

quint testはreservationブロック内の具体例を3件まとめて実行します。

  reservation
    ok soldOutTest passed 1 test(s)
    ok cancelRestoresStockTest passed 1 test(s)
    ok cancelUnknownIdTest passed 1 test(s)

  3 passing (10ms)

ここまでで、仕様は性質と具体例の両面から検査済みになりました。

仕様からトレースを出力し、中身を見る

quint runに--out-itfを付けると、シミュレータが辿った実行例を、ITF（Informal Trace Format）というJSON形式で書き出せます。この一本一本が、そのままテストケースです。

mkdir -p traces  # --out-itf は出力先ディレクトリを自動で作らない
npx quint run spec/reservation.qnt --backend typescript \
  --max-steps 5 --n-traces 3 --max-samples 3 --seed 42 \
  --out-itf 'traces/t_{seq}.itf.json'  # トレースを3本、ITF形式で出力

出力先ディレクトリが存在しないと--out-itfは失敗するため、mkdir -p tracesを先に実行しています。--seedを指定すると--max-samplesの既定値が1になるため（npx quint run --helpで確認）、トレースを複数本出すときは--max-samplesを--n-traces以上に指定してください。

出力されたtraces/t_0.itf.jsonのstatesを抜粋すると、次のようになっています。

{
  "lastRequest": { "tag": "Start", "value": { "#tup": [] } },
  "lastStatus": { "#bigint": "0" },
  "nextId": { "#bigint": "1" },
  "reservations": { "#map": [] },
  "stock": { "#bigint": "3" }
},
{
  "lastRequest": { "tag": "Cancel", "value": { "#bigint": "2" } },
  "lastStatus": { "#bigint": "404" },
  "stock": { "#bigint": "3" }
}

整数は{"#bigint": "2"}という形で、値は文字列です。Mapは{"#map": [[キー, 値], ...]}という組の配列です。Requestのような直和型は{"tag": ..., "value": ...}という形です。テストはこの形をJSの値に戻してから使います。

lastRequestを仕様の状態に加えた理由もここで説明します。Quintには--mbtオプションがあり、各状態に実行されたaction名（mbt::actionTaken）を付けて出力できます。しかし確認環境のTypeScriptバックエンドでは、初期状態以外のmbt::actionTakenが空文字列で出力され、どの操作が起きたかをトレースから判別できませんでした。そこで本記事では、リクエストを仕様の状態として明示的に記録する方式を取っています。この方式はバックエンドに依存しない点が利点です。

ITF を JS の値に戻すデコーダを書く

test/itf.tsに、#bigint・#map・#tup・#setをJSの値に変換する関数を用意します。

export type Value =
  | bigint | string | boolean
  | Value[]
  | Map<Value, Value>
  | Set<Value>
  | { tag: string; value: Value }
  | { [key: string]: Value }

export function decode(v: unknown): Value {
  if (typeof v === 'string' || typeof v === 'boolean') return v
  if (typeof v === 'number') return BigInt(v)
  if (Array.isArray(v)) return v.map(decode)
  if (v && typeof v === 'object') {
    const o = v as Record<string, unknown>
    if ('#bigint' in o) return BigInt(o['#bigint'] as string)       // 整数
    if ('#tup' in o) return (o['#tup'] as unknown[]).map(decode)    // タプル
    if ('#set' in o) return new Set((o['#set'] as unknown[]).map(decode)) // Set
    if ('#map' in o) {
      // Map は [キー, 値] の組の配列で表される
      return new Map(
        (o['#map'] as [unknown, unknown][]).map(([k, val]) => [decode(k), decode(val)]),
      )
    }
    // 直和型（tag/value）やレコードは、キーごとに再帰的に変換する
    const out: Record<string, Value> = {}
    for (const [k, val] of Object.entries(o)) {
      if (k.startsWith('#')) continue // #meta などの補助情報は読み飛ばす
      out[k] = decode(val)
    }
    return out
  }
  throw new Error(`unknown ITF value: ${JSON.stringify(v)}`)
}

#metaのような補助情報は読み飛ばし、値だけを素のJSに戻しています。

実装より先に、仕様からテストを書く

ここからはTDDで進めます。仕様はすでに検査済みなので、「正しい振る舞い」は仕様として手元にあります。実装はまだ一行もありません。

import { execFileSync } from 'node:child_process'
import { mkdtempSync, readdirSync, readFileSync } from 'node:fs'
import { tmpdir } from 'node:os'
import { join } from 'node:path'
import { describe, expect, test } from 'vitest'
import { createApp } from '../src/app'
import { decode } from './itf'

// ---------- 1. Quint にトレースを生成させる ----------
const N_TRACES = 20
const outDir = mkdtempSync(join(tmpdir(), 'quint-traces-'))
execFileSync('npx', [
  'quint', 'run', 'spec/reservation.qnt',
  '--backend', 'typescript',
  '--max-steps', '15',
  '--n-traces', String(N_TRACES),
  '--max-samples', String(N_TRACES),
  '--invariants', 'stockNeverNegative', 'stockIsConserved',
  '--out-itf', join(outDir, 'trace_{seq}.itf.json'),
], { stdio: 'pipe' })

// ---------- 2. 仕様の状態の型（decode後の形） ----------
type SpecState = {
  stock: bigint
  reservations: Map<bigint, string>
  lastRequest: { tag: 'Start' | 'Reserve' | 'Cancel'; value: unknown }
  lastStatus: bigint
}

const traceFiles = readdirSync(outDir).filter((f) => f.endsWith('.itf.json')).sort()

// 観測用エンドポイントを呼ぶ。200以外なら、JSONとして読む前にその事実で失敗させる
async function observe(app: ReturnType<typeof createApp>, path: string, step: number) {
  const res = await app.request(path)
  expect(res.status, `step ${step}: GET ${path}`).toBe(200)
  return res.json()
}

// ---------- 3. トレースを1本ずつHonoアプリに再生する ----------
describe('reservation API conforms to Quint spec', () => {
  for (const file of traceFiles) {
    test(`replay ${file}`, async () => {
      const trace = JSON.parse(readFileSync(join(outDir, file), 'utf8'))
      const states = trace.states.map(decode) as SpecState[]
      const app = createApp(Number(states[0].stock)) // 初期状態から実装を作る
      for (const [i, s] of states.entries()) {
        const req = s.lastRequest

        // (a) 仕様が受けたリクエストを、そのままAPIに送る
        let res: Response | undefined
        if (req.tag === 'Reserve') {
          res = await app.request('/reservations', {
            method: 'POST',
            headers: { 'Content-Type': 'application/json' },
            body: JSON.stringify({ user: req.value }),
          })
        } else if (req.tag === 'Cancel') {
          res = await app.request(`/reservations/${req.value}`, { method: 'DELETE' })
        }

        // (b) ステータスコードが仕様と一致するか
        if (res) {
          expect(res.status, `step ${i}: ${req.tag}(${req.value})`).toBe(Number(s.lastStatus))
        }

        // (c) 観測できる在庫数が仕様と一致するか
        const stock = (await observe(app, '/stock', i)).stock
        expect(stock, `step ${i}: stock`).toBe(Number(s.stock))
      }
    })
  }
})

app.request()は、Honoのアプリに対してサーバーを起動せずにHTTPリクエストを送れるメソッドです。observeは、レスポンスのステータスコードが200でなければJSONとして読む前にその事実で失敗させる小さな関数です。これを挟まずに直接.json()を呼ぶと、存在しないルートでHonoが返す本文404 Not FoundはJSONとして解釈できず、SyntaxErrorになります。結果として、仕様の言葉で失敗の理由が分かりません。

src/app.tsにはまだテンプレートのGET /しかないため、このテストは失敗します（Red）。

骨組みだけ作り、失敗の中身を読む

テストが求める最小の形だけをsrc/app.tsに書きます。観測用の2つのエンドポイントだけを足し、予約と取消の実装はまだ行いません。

import { Hono } from 'hono'

export function createApp(initialStock: number) {
  let stock = initialStock
  const reservations = new Map<number, string>()
  const app = new Hono()

  // 観測用：在庫数
  app.get('/stock', (c) => c.json({ stock }))
  // 観測用：予約一覧
  app.get('/reservations', (c) =>
    c.json([...reservations].map(([id, user]) => ({ id, user }))),
  )
  return app
}

この状態でテストを実行すると、失敗はすべて予約（Reserve）に関するものになります。POST /reservationsのルートが未実装のため、Honoは404を返します。仕様が期待する201とは食い違う。次に何を実装すべきかは、テストが仕様の言葉で示します。

存在しないIDへの取消（仕様では404）は、この時点でも偶然通ります。ルート自体が無いためHono既定の404が返り、たまたま仕様と一致しているだけです。ステータスだけの比較では、この種の偶然の一致は見抜けません。

予約を実装する

失敗が指している予約だけを実装します。

app.post('/reservations', async (c) => {
  const { user } = await c.req.json<{ user: string }>()
  if (stock <= 0) {
    return c.json({ error: 'out of stock' }, 409) // 在庫切れ
  }
  const id = nextId++
  reservations.set(id, user)
  stock--
  return c.json({ id, user }, 201) // 予約を作成
})

予約のルートを足すだけで成立します。その場合に残る食い違いはすべて取消関連になります。取消のルートがまだ未実装で、仕様の期待する204を返せないためです。失敗メッセージの中身で、実装の進み具合を読むことができます。

予約と取消を一度に実装しても構いません。実際の確認ではPOSTとDELETEを同時に足し、この中間状態を経ずにそのまま次の節のGreenになりました。

取消を実装する（Green）

DELETE /reservations/:idを追加します。

app.delete('/reservations/:id', (c) => {
  const id = Number(c.req.param('id'))
  if (!reservations.has(id)) {
    return c.json({ error: 'not found' }, 404) // 該当する予約がない
  }
  reservations.delete(id)
  stock++
  return c.body(null, 204) // 取消が成功、本文なし
})

トレース20本の再生がすべて通ります。テストが通ったことに意味があるかは、トレースが振る舞いを網羅しているかで決まります。今回と同じ条件（20本、各15ステップ）で生成したトレース内のlastStatusを数えると、201や404など複数のステータスコードと初期状態の0が、いずれも複数回現れました。

実装のバグが検出されることを確かめる

最後に、このテストが実装の誤りを本当に捕まえるかを確かめます。在庫切れ判定を書き換え、在庫0でも予約できてしまう実装に差し替える、という手順です。

- if (stock <= 0) {
+ if (stock < 0) {

意図的に壊した実装でテストを再実行します。

npm test

20本中19本のトレースで失敗し、どのステップで何を送って何がずれたかが次のように表示されます。

AssertionError: step 12: Reserve(alice): expected 201 to be 409

「在庫切れなら409」という期待値は、テストコードに一行も書いていません。期待値はすべて仕様から来ており、仕様を変えればテストの期待値も自動で変わります。仕様と実装のどちらかがずれれば、このテストが落ちることで、仕様検査として機能していることが分かります。

まとめ

設計を仕様として書いて機械に検査させれば、実装を書く前に誤りを見つけられます。同じ仕様からテストの期待値も取り出せるため、実装のテストを書く段になって書き手自身の思い違いが紛れ込む余地もありません。Quintは、この2つを1つの仕様でまとめて行うための道具の1つです。

在庫予約APIという小さな題材で、この流れを一通り確認しました。仕様の条件を変えれば、npm testの期待値もそのまま変わります。quint run自身が出力するとおり、--max-stepsや--n-tracesを増やすと、今回の20本では現れなかった状態も再生可能です。

本記事のテストは、app.request()でHTTPリクエストとして送り、Honoのルーティングを含めて丸ごと検査します。トレースの本数や仕様の複雑さが増えると、HTTP越しの往復が積み重なり、実行時間に効いてきます。ルーティングを経由せずドメインのロジックを直接呼ぶ、より狭い単位のテストでも同じ検査は可能です。