こんにちは！ラクスル事業部でWebエンジニアをしています井口です。
今回、2026/4/22~4/24にかけて開催されたRubyKaigi 2026に参加してきました。
私自身、今回が初めてのRubyKaigi参加だったのですが、新たな交流や、難しくも面白い新技術が数多くあり、非常に刺激を受けた3日間でした。
このブログでは、そんな数あるセッションの中から、特に今のAI時代だからこそ必要になってくる「生成コードの検証」に焦点を当てたセッションの内容をまとめ、深堀りしたいと思います。
そのセッションは @ohbarye さんの From Formal Specification to Property Based Testです。
実は社内でも、Coding Agentが良い成果物を作るためには検証ループを回す必要があり、検証方法の次なる打ち手として「Property Based Testing」（以降、PBTとします。）が提唱され始めています。事前に社内でも用語が出始めていたからこそ気になっていたセッションでもありました。
なぜ PBT なのか
旧来からあるソフトウェア開発のワークフローとして、プログラマーが仕様・実装・テストを書き、テストが実装を検証するという流れが一般的です。
そこで、重要なことは
- 書き起こされている仕様が正しいか、正しいことをどのように検証するのか
- テストが実装をどうやって検証するのか
というところです。
確かに、AIやCoding Agentで指示する際に渡す情報である仕様が間違っていれば、当然、生成される成果物も誤ったものになります。また、テストもフレーキーなものであれば、実装が誤ったものであることを検出できず、バグを本番環境にデプロイしてしまうことに繋がりかねません。
これらを解決し、品質保証しつつ、より良い開発サイクルを回すための方法の1つがPBTになるわけです。
実際、ラクスルの開発現場でもAIによるコード生成を試す中で、「動くコードはすぐに生成されるが、複雑な業務ロジックにおいてAIが織り交ぜてくるバグをどのように見抜くのか」が課題になりつつあります。AIへの指示は自然言語で行っている以上、細かいエッジケースの仕様は曖昧になりがちであり、AIが「よしなに」判断しているケースがよくあります。
形式仕様とPBTの概要
こちらでは聞き馴染みのない形式仕様とPBTについて説明します。（既にご存知の方は読み飛ばしていただいて大丈夫です！）
1. 形式仕様
形式手法は、数学や論理学をベースにして、ソフトウェアやハードウェアシステムの仕様記述や検証を行う手法の総称です。そして、その中でAlloyといったプログラム言語を用いて、システムの振る舞いを厳密に記したものを形式仕様といいます。
例えば、ECサイトでよくある仕様である「商品の在庫引き当てロジック（購入ボタンが押されたら販売可能在庫を1つ減らして出荷待ち在庫を1つ増やす）」をAlloyで表現すると、以下のようになります。
// 販売可能在庫（available）と、出荷待ち在庫（allocated）を持つInventoryモデルの定義
sig Inventory { available: Int, allocated: Int }
// 在庫を引き当てる（Allocate）時の仕様（ビジネスロジック）
pred Allocate [i, i': Inventory] {
// 【ガード条件】販売可能在庫が0より大きい場合のみ、この処理が実行できる
i.available > 0 implies
// 【状態遷移】販売可能在庫を1つ減らし、出荷待ち在庫を1つ増やす
i'.available = i.available - 1 and
i'.allocated = i.allocated + 1
}
自然言語で記述された仕様には、例外パターンと言ったエッジケースで矛盾が生じたり、解釈が曖昧になりがちです。
しかし、このような形式仕様で記述すると、数学的な検証（モデル検査）ができるため、「コードを1行も書く前の段階」で、この仕様自体に矛盾やバグ（例：在庫がマイナスになってしまうケースがないか等）がないかをチェックできるのが最大の強みです。
2. PBT
形式仕様に基づき、実装されたプログラムを検証するのがPBTです。
従来のテスト（RSpecの it ブロックなど）は「在庫数1のとき購入したら在庫数0になる」という個別の具体例を検証しますが、PBTは「そのプログラムが常に満たすべき普遍的な特性（Property）」を記述します。
例えば先ほどの「在庫引き当て機能」のテストであれば、以下のように定義できます。
何度在庫引き当てを繰り返しても、『販売可能在庫 ＋ 出荷待ち在庫』の合計値は、最初の総在庫数と常に完全に一致すること
あとはテストツールが、人間が思いつかないようなランダムな入力値や操作順序（在庫がゼロの状態でさらにキャンセルが走る、大量の注文が同時に来るなど）を数百〜数千通り生成して、実装を徹底的に検証してくれます。
また、バグを見つけた場合はそれを再現する「最小の条件（反例）」を自動で探索して報告してくれるShrinkingという機能もあります。
PBTの手法自体のメリットは以前から語られてきましたが、今、重要性が高まってきている背景には、AIやCoding Agentの台頭があります。
TDDのように先にテストを書いてからAIにアルゴリズムの実装を依頼する場合、従来の具体例を並べたテストだけだと、AIが「その特定のテストデータだけをパスするような実装」を出力してくるリスクがあります。
「本当に仕様の特性を満たした正しい実装になっているか」を検証するためのテストハーネスとして、今PBTの価値が高まってきています。
品質保証されたソフトウェア開発方法
形式仕様とPBTを組み合わせることで、より堅牢なソフトウェア開発ができそうに感じます。しかし、AIがPBTを記述する場合、間違ったテストコードを生成したときに悪い実装が生成され、結局バグを見逃すことになってしまいかねません。
そこで、あるべき理想のフローとしては@ohbaryeさんのスライドにもあるように、以下になります。
- 人間が仕様を厳密に考え、形式仕様に起こす（仕様の正しさを検証）
- その形式仕様からPBTのテストコードを自動生成する
- 生成されたPBTを使って、AIや人間が書いた実装コードを厳密に検証する
この「形式仕様からPBTを自動生成する」という部分を解決するために開発されたツールが spec-to-pbt です。spec-to-pbtの内部仕様や設計思想については、スライド資料や後に公開される発表動画をぜひご覧ください！
先ほどの形式仕様を説明したセクションで示した「商品の在庫引き当てロジック」を用いて、RailsのService ObjectをPBTで検証してみます。
形式仕様を書く
商品の在庫引き当てロジックを、Alloyで記述すると、次のようになります。形式仕様を説明したセクションで示されたものから、状態を追加してみました。
Allocate は販売可能在庫を1減らし、出荷待ち在庫を1増やします。Deallocate はその逆です。どちらの操作でも available + allocated の合計は変わらない、というのが今回検証したい性質です。
人間はこの部分の本質的な仕様を厳密に考えることに集中します。
module inventory_allocation
sig Inventory {
available: one Int,
allocated: one Int
}
-- Purchase allocation moves one unit from available stock to allocated stock.
pred Allocate[i, i': Inventory] {
#i.available > 0 implies
#i'.available = sub[#i.available, 1] and
#i'.allocated = add[#i.allocated, 1]
}
-- Cancellation returns one allocated unit to available stock.
pred Deallocate[i, i': Inventory] {
#i.allocated > 0 implies
#i'.available = add[#i.available, 1] and
#i'.allocated = sub[#i.allocated, 1]
}
fact NonNegative {
all i: Inventory | #i.available >= 0 and #i.allocated >= 0
}
assert TotalConserved {
all i, i': Inventory |
(Allocate[i, i'] or Deallocate[i, i']) implies
add[#i.available, #i.allocated] = add[#i'.available, #i'.allocated]
}
Railsアプリケーションを用意する
最小構成のRailsアプリを作り、テスト用にpbtとrspec-railsを入れます。
pbtというGemは、@ohbarye さんが開発しているRuby向けのPBT実行ツールです。こちらのツールの詳細は、RubyKaigi 2024の講演Unlocking Potential of Property Based Testing with Ractorをご確認ください。
rails new inventory-pbt-demo --minimal --skip-javascript --skip-hotwire
ruby "4.0.0"
group :development, :test do
gem "rspec-rails"
end
group :test do
gem "pbt", "0.6.0"
end
scaffold(ひな形)を生成する
spec-to-pbtのリポジトリから、Railsアプリのspec/pbt配下にscaffoldを生成します。
spec-to-pbtは記事公開時点ではRubyGems未公開のため、GitHubからcloneしてCLIを使いました。
bin/spec_to_pbt /path/to/inventory_allocation.als \
--stateful --with-config \
-o /path/to/inventory-pbt-demo/spec/pbt
生成される主なファイルは次の2つです。
inventory_allocation_pbt.rb: 再生成可能なPBT scaffoldinventory_allocation_pbt_config.rb: Rails側の実装に接続するための設定
spec-to-pbtでは、生成されたscaffoldを直接作り込むより、*_pbt_config.rb と*_impl.rbで実装への接続を管理するのが基本方針です。
RailsのService Objectに接続する
Rails側の実装は、通常のService ObjectとしてAIに実装してもらいました。
module Inventory
class Stock
attr_reader :available, :allocated
def initialize(available:, allocated: 0)
@available = available
@allocated = allocated
end
def allocate!
raise "no available stock" if @available <= 0
@available -= 1
@allocated += 1
nil
end
def deallocate!
raise "nothing allocated" if @allocated <= 0
@available += 1
@allocated -= 1
nil
end
def snapshot
{ available: @available, allocated: @allocated }
end
end
end
Rails側の実装（Service Object）とAlloyのcommandとの対応付けは、人間ないしAIが*_pbt_config.rbで行う必要があります。
InventoryAllocationPbtConfig = {
sut_factory: -> { Inventory::Stock.new(available: 10, allocated: 0) },
initial_state: { available: 10, allocated: 0 },
command_mappings: {
allocate: {
method: :allocate!,
verify_override: ->(after_state:, observed_state:, **) do
raise "Expected observed inventory after allocate to match model" unless observed_state == after_state
end
},
deallocate: {
method: :deallocate!,
verify_override: ->(after_state:, observed_state:, **) do
raise "Expected observed inventory after deallocate to match model" unless observed_state == after_state
end
}
},
verify_context: {
state_reader: ->(sut) { sut.snapshot },
}
}
これで、Alloyから推論されたモデル状態とRailsのService Objectの実状態を比較できます。
そうして、RSpecを実行してみます。
bundle exec rspec spec/pbt/inventory_allocation_pbt.rb
正しい実装では green になりました。
1 example, 0 failures
バグを入れてみる
次に、allocate! で available だけを減らし、allocated を増やし忘れる実装にしてみます。
def allocate!
raise "no available stock" if @available <= 0
@available -= 1
nil
end
この状態で同じ PBT を実行すると、1回目の操作列で失敗しました。
Pbt::PropertyFailure:
Property failed after 1 test(s)
seed: 1
counterexample: [#<Pbt::Stateful::Step command=:allocate, args=nil>]
Shrunk 4 time(s)
Got RuntimeError: stateful step 0 (allocate): Expected observed inventory after allocate to match model [args=nil]
通常の具体例に基づくテストでもこのバグは見つけられますが、ここで重要なのは「人間が具体例を並べた」のではなく、「形式仕様から作られたモデル」と「実装の状態」がズレたことをPBTが検出している点です。
AI に実装を依頼した場合でも、availableだけを減らすような「それっぽく動くが仕様を満たしていない実装」を、この検証ループに通すことで検出できます。
試してみた感想
思っていたよりも簡単にRailsアプリケーションにPBTを組み込むことができました。通常の開発では具体例に基づくテストを主に書いていますが、プロダクトのメインドメインやステータスフローではPBTで堅牢にテストし、それ以外は具体例に基づくテストと併用すればよさそうだと感じました。
また、生成されるのは完成品のテストではなくPBTのひな形ですが、その接続作業は想定より少なく、検証ループの土台として十分使えそうだと感じました。
まとめ
このAI時代だからこそ、生成されたコードへの検証はより良いものにしていく必要があります。
今回のセッションでは、その一例として、検証済みの形式仕様・実装を検証するために生成されたPBT・AI Coding Agentを用いた、より品質保証されたソフトウェア開発方法が紹介されました。
PBTは、旧来だと「人間が頑張って厳密な仕様を書き、マシンにチェックさせる」というストイックな開発手法であったと思います。しかし今回の発表を聞いて、「人間は本質的な仕様を厳密に考えることに集中し、そこからツールが決定論的にテスト（PBT）を生成し、AIが生成した実装のバグを徹底的に検証する」開発効率と品質保証の両方を兼ね備えた手法へと進化していくところに未来を感じました。
本ブログで用いたspec-to-pbtは、Rails側の実装との接続はConfigで人間ないしAIが行わないといけません。stateless 向けの自動生成もありますが、対象は限定的なパターンに留まります。今後の進化にも注目していきたいと思います。
参考
