開発をシフトレフトせよ――形式仕様でAIと事前に合意する開発のすすめかた
AI への指示書は自然言語で書きます。
書いた本人には明確に見えますし、AI も分かったという顔をして実装を始めます。
その結果、できあがったものが思っていたものではないことがあります。
なぜなら、自然言語は解釈が揺れるからです。
私が開発している OSS の TAKT では、この揺れを実行前の対話で潰しています。
具体的には、アシスタントとタスクを詰めて合意した内容を、指示書にまとめてからエージェント群に渡すようにしています。
この指示書の受け入れ条件はこれまで Gherkin で書かせてきました。
v0.61.0 でここに形式仕様モードという設定を足しました。
有効にすると、指示書の要件を Quint と Alloy という記法でも表現するようになります。
形式手法は正しさが欲しい場面で昔から使われてきた道具です。
ただ実務で常用するには仕様を書いて維持するコストが高く、採用できないという結論になりがちの代物でした。
有効であることは間違いないが運用するのが重い。
そんな形式手法ですが、昨今は AI の時代です。
書く手間を AI が引き受けられるなら、実用可能ではないだろうか。
これが、この手法に取組むきっかけになったのです。
TAKT の形式仕様モードの仕組み
TAKT では TUI を開くとデフォルトで形式手法を利用するかを確認されます。
なお、この設定は config.yaml に assistant.formal_spec として設定もできます。
# ~/.takt/config.yaml（プロジェクトの .takt/config.yaml でも可）
assistant:
formal_spec: 'Y/n' # true / false / 'Y/n' / 'y/N'（既定は 'y/N'）
'Y/n' と 'y/N' は既定回答つきの質問で、対話セッションの最初に一度だけ「形式仕様モード（Alloy, Quint）を有効にしますか？」と聞かれます。
true と false は質問なしでそのまま使われます。
有効にしたときの記法の分担はこうなります。
Gherkin には観測可能な振る舞い、つまり外から見える挙動を Given/When/Then の具体的なシナリオで書きます（これは形式仕様モードと関係なく、開発タスクなら常時出力されます）。
ただしシナリオは代表例を挙げる書き方で、全ケースを網羅する保証はありません。
Quint が受け持つのは振る舞いの一般則です。
システムをステートマシンとして捉え、すべての入力と状態遷移に対する規則を書きます。
元になっているのは、AWS などが分散システムの設計検証に使ってきた TLA+ という言語で、その考え方をプログラマになじみやすい構文で書けるようにしてあります。
Alloy はデータ構造を受け持ちます。
何が登場してどう関係するかを定義して、常に成り立つべき制約を宣言します。
こちらは MIT で作られた、ソフトウェア設計をモデル化するための言語です。
どちらも本来は検証器とセットで使う道具ですが、TAKT では記法として使います（後述）。
実際に生成された指示書
形式仕様の設定を有効にして、TAKT 自身の修正タスクを1件流したときの実行を例にします。
題材は設定ディレクトリのパス衝突を防ぐガードの追加です。
リンク先の Issue の上のほうを見てもらうと、背景・目的、作業範囲、優先度といった決まった見出しが並んでいるのが分かります。
自由文で書かれた仕様書はぶれやすく、読みづらいものです。
というか読みたくない。
設計書というフォーマットが使い古されている理由はこのためです。
TAKT では Gherkin や Quint や Alloy をその代わりとします。
TAKT のグローバル設定は ~/.takt、プロジェクト設定はカレントディレクトリの .takt にあり、ホームディレクトリで起動したりシンボリックリンクを張ったりすると両者が同じ実体を指してしまいます。
この状態を起動時に検出して止めるガードを入れるというタスクです。
対話では、存在しないパスをどう比較するか（存在すれば realpath、なければ論理パスの正規化）、--help と --version は衝突していても通すこと、どこまでを対象外とするか、といった判断を詰めました。
合意して指示書を作らせると、受け入れ条件がまず Gherkin で出てきます（抜粋）。
Feature: グローバル設定とプロジェクト設定のパス衝突ガード
Scenario: パス衝突時は初期化前に非ゼロ終了する
Given TAKT_CONFIG_DIR が未設定で、カレントディレクトリがホームディレクトリである
When takt をサブコマンド付きで起動する
Then プロジェクト初期化の前に非ゼロ終了する
And 衝突パス・原因・対処方法を含むエラーが表示される
Scenario Outline: メタコマンドは衝突時も動作継続する
Given 設定パスが衝突している
When takt を <flag> 付きで実行する
Then 正常に動作して終了する
Examples:
| flag |
| --help |
| --version |
Gherkinはほとんど自然言語なのでそのまま読むことができますね。
Given When Then の意味さえわかれば容易だと思います。
続いて同じ要件を Quint で書くとこうなります（コメントは解説用に私が足したものです。Alloy 版も同様）。
// module はこの仕様のまとまり
module taktConfigCollisionGuard {
// 起動の結果は「続行」か「エラー終了」の2つ
type Outcome = Proceed | ExitNonZero
// パスが同じなら衝突、という判定
pure def collides(globalReal: str, projectReal: str): bool =
globalReal == projectReal
// 起動時にどうするかのルール
// --help / --version（isMetaOnly）なら常に続行、
// パスが衝突していたらエラー終了、それ以外は続行
pure def startupOutcome(isMetaOnly: bool, globalReal: str, projectReal: str): Outcome =
if (isMetaOnly) Proceed
else if (collides(globalReal, projectReal)) ExitNonZero
else Proceed
// ここから下は、このルールを3つのケースで確かめるテスト
// --help はパスが衝突していても続行する
run metaOnlyAlwaysProceedsTest =
assert(startupOutcome(true, "/home/u/.takt", "/home/u/.takt") == Proceed)
// 衝突していたらエラー終了する
run collisionExitsTest =
assert(startupOutcome(false, "/home/u/.takt", "/home/u/.takt") == ExitNonZero)
// パスが違えばふつうに続行する
run distinctPathsProceedTest =
assert(startupOutcome(false, "/home/u/.takt", "/home/u/proj/.takt") == Proceed)
}
起動時にどうなるかを1つの関数で決めて、代表的な3ケースをテストで確かめる形です。
今回のガードは起動時に一度判定するだけで状態遷移がないので、Quint としてはかなり簡素な部類ですね。
Alloy 版はこうです。
-- sig は「登場するもの」の宣言。Path はパスを表す
sig Path {}
-- 起動の結果は「続行」か「エラー終了」のどちらか
abstract sig Outcome {}
one sig Proceed, ExitNonZero extends Outcome {}
-- takt の起動1回。3つの値を持つ
sig Invocation {
globalReal: one Path, -- グローバル設定のパス（解決後）
projectReal: one Path, -- プロジェクト設定のパス（解決後）
outcome: one Outcome -- その起動がどうなったか
}
-- 起動のうち --help / --version だったもの
sig MetaOnly in Invocation {}
-- fact はいつでも成り立つルール。ここがガード本体
-- エラー終了するのは「--help / --version ではない」かつ「パスが一致」のとき
-- それ以外でエラー終了することはない。iff はこの両方をまとめて言う
fact Guard {
all i: Invocation |
i.outcome = ExitNonZero iff
(i not in MetaOnly and i.globalReal = i.projectReal)
}
-- assert は上のルールから当然こうなるはず、という主張
-- 検証器はこれが破れる例（反例）を探す
-- --help / --version は必ず続行する
assert MetaAlwaysProceeds { all i: MetaOnly | i.outcome = Proceed }
-- パスが違えば必ず続行する
assert DistinctPathsProceed {
all i: Invocation | i.globalReal != i.projectReal implies i.outcome = Proceed
}
-- 登場するものが4個までの組み合わせを全部試して反例を探せ、という指示
check MetaAlwaysProceeds for 4
check DistinctPathsProceed for 4
fact Guard は、非ゼロ終了するのはメタコマンド以外でパスが一致したときだけ、それ以外では非ゼロ終了しない、と言っています。
--help の例外まで含めたガードの全体像が iff の1文に収まっています。
自然言語で同じことを言おうとすると、例外の但し書きが3か所くらいに散らばるやつです。
構文は予約語が多めですが、コメントがあれば読めると思います。
このコメントを付ける機能も TAKT に同梱されています。
下流のエージェントがどう使ったか
指示書はそのままワークフローに流れるので、計画やレビューを担当するエージェントも Quint と Alloy を読みます。
今回の実行（ワークフローはビルトインの takt-default）でどう扱われたかを成果物のレポートから拾ってみます。
レビューの指摘を取捨選択する裁定エージェントは、レポートの中で要件を12項目に分けて、項目ごとに判定の根拠を書いていました。
その根拠の欄に「確定仕様、Quint・Alloy」のように、Quint と Alloy が何度も出てきます。
修正が正しいかを確かめる検証エージェントも、修正計画を元の要求や Quint/Alloy と突き合わせていて、レポートには Alloy で定義した MetaOnly がそのまま出てきます。
これは特別に参照するよう指示したわけではありません。
TAKT のレビューは記録された証跡から判定する方針をとっているので、エージェントが答え合わせの相手に形式仕様を自分で選んだ形です。
自然言語の指示書だけだと、検証エージェントは要件を満たしたかどうかを文章の解釈で判定するしかありません。
iff の1文があれば、条件と実装を突き合わせて確認できます。
検証器は回していない
Quint と Alloy は本来検証器とセットの道具です。
現状の TAKT はその検証器を回していません。
quint run も Alloy Analyzer も走らせていませんし、構文の正しさもプロンプトで要求しているだけです。
形式手法に詳しい方から見れば片手落ちに見えるはずで、そのとおりです。
これらの手法を利用する TAKT での目的は、走らせる前に AI と方針を合意しておくことです。
たとえば iff の1文は例外の扱いが決まっていないと書けません。
書かせようとすれば、--help のときはどうするのかを対話の時点で決めることになります。
決めた結果は指示書に残り、先ほど見たとおり下流のレビューや検証の答え合わせに使われます。
仕様に書いたケースどおりに実装が動くかは、ワークフローで何度も確かめられています。
また、TAKT のビルトインワークフローのほとんどがテストを先に記述するステップがあり、そこで受け入れ条件として Quint や Alloy を満たすような実テストが作成されることになります。
今回の実行でも、Quint の3ケースとほぼ同じ境界が vitest のテストとして定義されていました。
検証器にしかできないのは、仕様そのものを総当たりで調べて、人も AI も思いつかなかった反例を見つけることです。
それは TAKT の範疇ではなさそうで、現状は手を付けていませんが、必要だと思ったら組み込んでいこうと考えています。
まとめ
形式手法が実務に広がらなかった理由のひとつが記述のコストであるとするなら、書き手が AI になった今はないに等しいでしょう。
指示書に Quint と Alloy を書かせるのは設定1行で、曖昧な点は実行前の対話で見つかるようになり、その後のレビューでも答え合わせに使われました。
これまでの開発では決定はなるべく先送りにするのが鉄則でした。
不確実性の高い段階で確定事項を決める行為は、手戻りの可能性を増やすだけだったからです。
しかしながら、現在の AI をベースとした開発では逆のことが起きています。
AI に指示を出して走らせると、人間が介入しないぶん、間違った方向に進んだときはとんでもないところにたどり着いてしまいます。
結果として大きな手戻りにつながります。
これを解決するためには、AI への指示であいまいな部分や合意できていない部分を実行前に洗い出す必要があります。
いままでは、細かい部分はコードを書きながら設計するようなやり方をしていました。
しかし、残念ながらコーディングに関与しなくなった今、これまで先送りできていたことの一部が先送りできなくなったわけで、マインドチェンジが求められます。
結果として、開発における意思決定はどんどん手前に寄っていく。
求められるのは開発のシフトレフトで、形式手法はそのための解法のひとつになると思っています。
TAKT にはこのやり方がそのまま入っています。
対話で合意を固めて、形式仕様つきの指示書を作り、計画からレビュー、マージ判定までをワークフローで回して、人間は結果を確認する。
この手法でがっつり開発したいと思った方は、ぜひ使ってみてください。
npm install -g takt
TAKT のユーザーコミュニティはこちらです！ 質問や要望などができます！
Discussion