# AIは「その通り」と言い、形式手法は「間違いだ」と言う

- 番組: [The Stack Overflow Podcast](https://ai-curator.jp/podcasts/shows/cmv3z5c1l00105o106qjscjap)（The Stack Overflow Podcast）
- 元のタイトル: AI says you’re right, formal methods say you’re wrong
- 配信日: 2026年10月16日
- 長さ: 28分
- 要約作成日: 2026年10月16日
- トピック: [#形式手法](https://ai-curator.jp/topics/%E5%BD%A2%E5%BC%8F%E6%89%8B%E6%B3%95) [#TLA+](https://ai-curator.jp/topics/TLA%2B) [#Quint](https://ai-curator.jp/topics/Quint) [#AIコーディング](https://ai-curator.jp/topics/AI%E3%82%B3%E3%83%BC%E3%83%87%E3%82%A3%E3%83%B3%E3%82%B0) [#モデルベーステスト](https://ai-curator.jp/topics/%E3%83%A2%E3%83%87%E3%83%AB%E3%83%99%E3%83%BC%E3%82%B9%E3%83%86%E3%82%B9%E3%83%88) [#スペック駆動開発](https://ai-curator.jp/topics/%E3%82%B9%E3%83%9A%E3%83%83%E3%82%AF%E9%A7%86%E5%8B%95%E9%96%8B%E7%99%BA)
- URL: https://ai-curator.jp/podcasts/cmvamvuju00004610rac5h0ol

## 要約

Stack Overflow Podcast で、Quint CEO の Gabriela Moreira が、TLA+ などの形式仕様言語がコードを書く前に設計上の欠陥を見つける仕組みを語った。TLA+ の上に開発者向け構文を載せた Quint の特徴、OpenHands の Kubernetes での競合状態の事例、AI 時代に仕様を誰が書き、誰が確認するのかという問題を扱う。モデルベーステストやトレース検証で、AI 生成コードを実運用のデータと突き合わせる方法も紹介された。

## ポイント

- TLA+ は曖昧さのない形式仕様言語で、Leslie Lamport が論文中の分散システムのアルゴリズムを正確に書くために作った。モデル検査器 TLC で性質を検証できる。
- Quint は TLA+ の表層構文を開発者向けに置き換え、ツールも追加したもの。OpenHands の競合状態の修正が不十分だと Quint が指摘し、本番でも実際に再発したという事例が紹介された。
- Gabriela は、AI が証明を書けるようになった現在の最大の問題は、誰が仕様を書くのかだと述べる。AI に仕様まで任せると、何を証明したのか分からなくなる恐れがある。
- Markdown によるスペック駆動開発は、不正確で実行もできず、大きなプロンプトにすぎないと批判している。仕様は実行して結果を見られることが重要だという立場である。
- 仕様を実コードに結びつける方法として、モデルベーステスト（モデルの挙動をコードで再生）とトレース検証（本番ログが仕様に許されるか確認）を挙げた。
- 仕様を書くだけでも、if に else が必須なため見落としが見つかる。Quint Studio はテストをログ付きで走らせ、トレース検証でテストの網羅状況を示す。

## 章立て

- [00:00] **ゲストの経歴と形式手法の印象** — Gabriela が計算機科学から TLA+ に出会った経緯と、形式手法が難しく見られがちな理由を語る。
- [02:03] **TLA+ とは何か** — 曖昧さのない形式仕様言語としての TLA+、Lamport による成り立ち、モデル検査器の役割を説明する。
- [05:15] **設計優先と Quint の事例** — 設計図の比喩、既存コードでも使える点、Quint の紹介と OpenHands の競合状態の事例を紹介する。
- [10:23] **証明支援系とAI時代の仕様** — Lean など証明支援系との違い、AI が証明を書く時代に誰が仕様を書くかという懸念、スペック駆動開発への批判を述べる。
- [16:47] **挙動中心で形式仕様に入る** — 仕様を実行可能な挙動の集合として捉える考え方と、仕様を書くことで見つかるバグを語る。
- [22:52] **開発ライフサイクルとテスト手法** — 設計段階での利用、モデルベーステスト、トレース検証、Quint Studio の取り組みを説明する。

## 解説記事

Stack Overflow Podcast の今回の回では、ホストの Ryan Donovan が Quint の CEO、Gabriela Moreira を迎え、形式仕様言語 TLA+ と、その派生である Quint を取り上げた。AI がコードを書く時代に、形式手法がどう役立つのかが主題である。

#### 形式仕様とは何か

TLA+ は、ソフトウェアが何をすべきか、何をしてはならないかを、曖昧さなく書くための形式仕様言語だと説明された。構文に厳密な意味論が与えられており、解釈の余地がない。分散システムの父として知られる Leslie Lamport が、自分の論文にも不正確さがあると気づき、共通言語として作ったという。

その後モデル検査器 TLC が実装され、書いた仕様が性質を満たすか機械で確認できるようになった。Gabriela は、モデル検査器を実行コードを生成しないコンパイラのようなものと説明する。実コードの検証ツールは対象が広すぎて限定的になりがちだが、TLA+ は範囲が狭いぶん多くを検査できるとも述べた。

#### Quint と「間違いだ」と言ってくれるツール

Quint は TLA+ の上に載せた別の構文で、数学記号が多い TLA+ より、AND や OR といったプログラマに馴染む書き方ができる。ツール面でも産業利用向けの拡張が加えられている。

具体例として語られたのが OpenHands の事例だ。Kubernetes のデプロイで競合状態が起き、アラートが頻発していた。修正を入れても結果が分かるまで数週間かかるため、Quint で検証すると、この修正では不十分なケースが残ると指摘された。実際に本番で同じ問題が再発し、その後 Quint が検証を通すまで修正案を試して出荷したという。Gabriela は、Claude や ChatGPT が「その通り」と言うのに対し、形式手法は「完全に間違っている」と言うと冗談めかした。さらに、AWS が TLA+ で積極的な最適化を自信を持って適用できた例にも触れた。

#### AI時代の最大の問題は誰が仕様を書くか

Lean や Coq のような証明支援系では、仕様に加えて証明も自分で書く必要があり、安全性が極めて重要な領域に限られていた。Gabriela は、今年は AI に証明を書かせられるようになり状況が変わったと述べる。一方で、仕様まで AI に書かせると、何を証明したのか分からなくなる点を最大の懸念として挙げた。

そのため Quint では、実行例を一つ出させる、対話的に確かめるなど、仕様の中身を理解するための機能を重視しているという。Markdown で書くスペック駆動開発には、不正確で検証も実行もできず、大きなプロンプトにすぎないと批判的だ。実行して結果を見て直すという反復の楽しさが失われるとも語った。

#### 挙動を入口に、仕様を実コードへつなぐ

Gabriela は、仕様を「システムが取りうる挙動（状態の列）の集合」として捉えることを、入口として勧める。口座残高の例では、「残高が負にならない」という性質を書き、モデル検査やシミュレーションで到達不能だと確かめられる。仕様を書くだけでも、Quint や TLA+ では if に else が必須なので、コードでは見えない未処理の分岐に気づける。セキュリティ監査では、ツールを走らせる前にバグを見つけることが多かったという。

仕様と本番コードの差を埋める方法は二つ紹介された。一つはモデルベーステストで、モデルの挙動をランダムあるいは指定して実コードで再生し、各ステップで一致を確かめる。もう一つはトレース検証で、本番ログを一つの挙動と見なし、仕様がそれを許すかを判定する。ただし本番から取れるデータの粒度には限りがあり、実装は難しいと述べている。

現在ベータ版の Quint Studio は、既存のテストをログ付きで実行し、トレース検証でどの挙動が試されているかを示す。たとえば入金後の出金がテストされていない、といった指摘ができるという。

#### まとめ

AI がコードも仕様も書く流れの中で、何を作るべきかという意図を人が確認する手段として、形式仕様の価値を訴える回だった。日本の開発者にとっては、仕様を挙動と性質で捉えて実行しながら確かめる考え方が実践しやすい。AI 生成コードを、本番ログやテストと突き合わせて検証する発想も参考になる。なお、挙動中心のアプローチが広く受け入れられるかは、Gabriela 自身も確信はないと述べている。

> この要約・解説記事は、元の音声の文字起こしをもとに AI（Claude）が日本語で作成したものです。出典: The Stack Overflow Podcast「AI says you’re right, formal methods say you’re wrong」