Quintとは？

Quint は、システムの「仕様」を実行可能なコードとして書き、バグがないかを自動検証してくれるツールです。 プログラムのバグを見つける方法といえば「テスト」が一般的ですが、テストは「思いついたケースしか確認できない」という限界があります。 Quintは「どんな状況でもこのルールが破れないか？」を自動で大量にシミュレーションしてくれます。

インストール

Node.jsが入っていればnpmで一発です。

npm install -g @informalsystems/quint

やってみた：銀行の送金システム

銀行でアリスとボブがお金を送り合うシステムを考えます。 「どんな送金を繰り返しても、お金の総量（200円）は変わらないはず」 これをQuintで書くとこうなります：

module bank {
  var alice: int
  var bob: int

action init = all {
    alice' = 100,
    bob'   = 100
  }

action aliceToBob = all {
    alice >= 10,
    alice' = alice - 10,
    bob'   = bob + 10
  }

action bobToAlice = all {
    bob >= 10,
    bob'   = bob - 10,
    alice' = alice + 10
  }

action step = any {
    aliceToBob,
    bobToAlice
  }

// 不変条件：お金の総量は常に200円
  val totalIsConserved = alice + bob == 200
}

バグを仕込んで検出させる

bob' = bob + 10 を bob' = bob + 20（10円送ったのに20円増える）に変えてみます。

quint run bank.qnt --invariant=totalIsConserved

結果：

[State 0] { alice: 100, bob: 100 }
[State 1] { alice:  90, bob: 120 }

[violation] Found an issue

1回の送金で即バグ検出。 合計が200円→210円に増えていることを見つけてくれました。 バグを直して再実行すると、何万回試しても [ok] No violation found になります。

どんな用途に向いている？

分散システムやブロックチェーンのプロトコル設計に特に向いています。Solana・Cosmos・Matter Labs（ZKSync）など、バグが致命的になるシステムで実際に使われています。 「特定の順序でリクエストが来たときだけ起きるバグ」は手書きテストでは見つけにくいですが、Quintのような仕様検証ツールなら機械的に探せます。 オープンソース（Apache 2.0）なので、興味があればぜひ試してみてください。