開発をシフトレフトせよ――形式手法でAIと事前に合意する開発のすすめかた

これは、AIへの指示書を自然言語で書くと実装がずれるという悩みに、形式手法で答えようとする開発の報告である。OSSのTAKTは、実行前にアシスタントとタスクを詰め、合意内容を指示書にまとめてからエージェント群に渡す。v0.61.0で加わった形式仕様モードは、その指示書の要件をGherkin、Quint、Alloyの3つの記法でも表現させる設定だ。有効化は設定ファイルのassistant.formal_specで決め、既定値はy/Nである。役割は分担されていて、Gherkinは外から見える振る舞いを具体例で書き、Quintは状態遷移の一般則を、Alloyはデータ構造と成り立つべき制約を受け持つ。題材は、グローバル設定とプロジェクト設定のパス衝突ガードだ。ホームディレクトリで起動したりシンボリックリンクを張ったりすると両者が同じ実体を指してしまうため、起動時に止める仕組みを仕様化した。

AIの鬼の視点で言えば、面白いのは形式手法が採用されなかった理由を正面から崩しにきている点だ。形式手法は正しさが欲しい場面では有効だが、仕様を書いて維持する手間が重く、結局採用できないという結論になりがちだった。著者はその手間をAIが引き受けられるなら実用になるのではないか、と問い直している。しかも検証器をフルに回すのではなく、記法として使うと割り切っているのが実務的だ。大事なのは形式仕様そのものより、実行前に人間とAIが「何を作るか」をずらさずに合意する場が生まれることである。読みたくない自然言語の設計書を、読める形の合意に変えたとも言える。

中小企業の現場に持ち帰るなら、Gherkinの「Given・When・Then」だけ覚えれば十分だ。AIに頼む前に「こうなったら成功」を具体例で三行書かせ、その場で読み返す。QuintやAlloyの記法は、そこから先の話である。