AI コーディング・ループにおける形式検証ゲート

日本語翻訳:

最も重要な発見は、アクセス制御の脆弱性が依然として最大のセキュリティリスクであり、モデル指示のみを頼ることは本質的に不安定であるという点です。モデルは規則を容易に忘れたり、権限を妄想したりする可能性があるためです。これを解決するために、Shen-Backpressure は脆い振る舞いのプロンプトを置き換え、静的型付けコンパイラによって強制される堅牢な構造的ソリューションを採用します。従来の手法とは異なり、このアプローチはメンバーシップチェックをばらばらなハンドラーコードから集約された構築境界へとシフトさせ、未承認アクセスを構造的に困難かつ高コストに違反させるようにしています。この方法は、静的型付け Lisp 言語である Shen と演算子計算式の型システムを利用し、テナントアクセスルールなどの厳格な権限付与不変量を強制します。開発プロセス中、ビルドループは決定論的な失敗データをプロンプトへフィードバックし、専用ツールが Go ストラクチャなどというターゲット言語のガード型を生成して、これらのセキュリティポリシーを固定化します。今後、このスケルトンには Claude Code や Cursor などの高度な LLL ハネスを組み込み、コード生成を自動化する予定です。この拡張では、型チェッカーとジェネレータを信頼できる計算基盤の一部として扱い、ガードコードへの未承認の手動編集を拒否します。結局のところ、ユーザーは指定された不変量が実際には偶然違反されることが不可能であるという監査可能な確実性を得るとともに、企業は Go、TypeScript、Python、Rust のような複数の言語をサポートする単一ツールの恩恵を受け、ハンドラーコードに散在するセキュリティ失敗を大幅に削減できます。

いくつか最も深刻なソフトウェアバグが、同時に最も退屈なのも事実です。ユーザーが他のテナントのデータを読み込むことを許してはなりません。これは誰も異議を唱えず、システム設計レビューにおいて「A 氏が B 氏の記録を読むこと」を防ぐための対抗意見を立てる者は一人もいません。にもかかわらず、「アクセス制御の不備」は依然として OWASP Top 10 の第 1 のカテゴリーとなっています。

これらのバグが製品に組み込まれてしまうのは、規則をシステムの誤った位置に配置したからであります。その規則はプロンプト（指示文）に置かれ、レビューチェックリストの項目にされ、「すべての将来のエンジニア」、そして今や「すべての将来的なモデル呼び出し」もその不変条件（invariant）を覚えていて正しく再適用するという共有された期待の中に存在しています。

この前提はもともと脆弱であり、AI がコードの大部分を生成する現在では outright に失敗します。当然のことを行っても構いません：規則を CLAUDE.md に置くこと、慎重なシステムプロンプトを作成すること、エージェントの指示に「認可（authorization）は非常に重要である」と加えることなどです。そのようにすべきなのは確かですが、モデルが 16,000 行ものコードを書き上げた後の真の問題は、「そのコードが望む通り動作していることをどのように知っているか」という点にあります。テストも役立ちますが、テストは実証的（empirical）でありすぎます。 tester とモデルが書き残すケースをチェックするに留まり、来週の誰かが追加するハンドラについて語ることはできません。

私は別のレバーを引きたいと考えています。率直に言えば私の賭けは次の通りです：広範なクラスの生産用ソフトウェアに対しては、「構造的なバックスプレッシャー（構造による制約）」の方が、エージェントの知能への漸進的改善よりも優れています。既存のモデルはすでにあなたのコードのほとんどを記述できますが、制限要因となっているのは「彼らが望むとおりに動作していることを知ることができるか」という点であり、その知識はモデルが構築する際の基盤（substrate）から得られ、より賢いモデルを待つことからは得られません。

Shen-Backpressure は、その賭けを検討するために私が構築したツールおよび方法論です。ここでは実行可能なデモを通じてそれが何を行うかを示し、続いてどのようにそれをあなたのプロジェクトのループに接続するかを示します。

振る舞いによるゲートと構造的なゲート

多くのプロンプトレベルの制約は「振る舞いによるゲート（behavioral gate）」です。モデルには「認可をスキップしないこと」「入力を検証すること」「共有ヘルパーを使用すること」などと伝えます。モデルはこれらの指示に十分な頻度で従っては有用ですが、同時に不十分な頻度で失敗し、その全体としての仕組みを不安定なものにします。振る舞いによるゲートは、モデルが規則を記憶し、適用範囲を認識し、局所的な文脈の重力的な引力に抗する能力に依存しており、さらに人間レビューヤーがコードベース全体を通じて同じ不変条件を維持しなければなりません。

一方、構造的なゲート（structural gate）は異なります。コンパイラ、型チェッカー、テストランナー、リンター、証明チェッカーなどです。それぞれがその前にあるアティファクト（生成された成果物）について具体的な答えを生み出します。その答えは完璧ではありませんが、それは現実であり、その範囲内ではコードが間違っていれば拒否します。

その「拒否」こそが目的です。これにより、仕事をモデルの指示領域から抜き取り、モデルが構築を続ける基盤へと移すことができます。トークンを費やしてモデルに不変条件を覚えておいてほしいと beg を代わりに、コード自体の配列を工夫し、偶然に違反されにくいようにします：最も重要とする属性を機械が検証できる形に変換し、実装へと投影し、そのチェックに対してループを跳ね返らせ、創発する成果物がそれを満たすまで続けます。

これが、Geoff Huntley の Ralph または論文『あなたのバックスプレッシャーを浪費しないでください』において使用される用語の意味における「バックスプレッシャー」が力を持つ理由です。前回のエラーが次のイテレーションにパイプされるとき、決定論的なゲート（deterministic gate）はループに、「フィーリング（vibes）」よりも固いものを押し返すための何かにします。そのループはもはやニッチなアイデアではなく、Codex CLI が現在

/goal

をリリースしており、OpenAI 自身による Ralph ループの解釈として、ターンを超えて目標を維持し、達成されるまで止まらずに拒否する仕組みを持っています。

基盤への移行

強制すべき不変条件は、通常は正確な表現が容易です。ユーザーは認証済みであり、テナントメンバーであり、かつそのリソースがそのテナントに属している場合のみ、リソースにアクセスできるといったことは、完全で有界された規則です。英語はそれを強制するための不適切な媒体です。

Shen-Backpressure は、その種類の規則を、モデルがターゲット言語の型、コンスストラクター、ゲートコマンドに対して記述しなければならない形において、機械に投影可能な形式に変換するために、静的型付けされた Lisp の一種である Shen を使用します。一度に仕様（spec）を書き、コードジェネレーター

shengen

がそれをターゲット言語へのガードタイプへ降下（lower）させます。モデルが Go や TypeScript を記述している場合でも、Shen が存在することを知る必要はありません。コンパイルできるコードであり、ゲートを通すだけの必要があります。

マルチテナント認証のための証明連鎖

マルチテナント API デモの心臓部である、

specs/core.shen

から抜粋されたものです：

(datatype jwt-token
  X : string;
  (not (= X "")) : verified;
  ============================
  X : jwt-token;
)
(datatype tenant-access
  Principal : authenticated-principal;
  Tenant : tenant-id;
  IsMember : boolean;
  (= IsMember true) : verified;
  ================================
  [Principal Tenant IsMember] : tenant-access;
)
(datatype resource-access
  Access : tenant-access;
  Resource : resource-id;
  IsOwned : boolean;
  (= IsOwned true) : verified;
  ================================
  [Access Resource IsOwned] : resource-access;
)

水平線が役目を果たします。線の上の前提条件は、下の結論が構築される前に満たされなければなりません。

resource-access

を得るには

tenant-access

と、リソースが所有されていることの証明が必要であり、

tenant-access

を得るには認証されたプリンシパルとメンバーシップの証明が必要です。完全な連鎖は

jwt-token

→

authenticated-user

→

tenant-access

→

resource-access

のようになります。完全な仕様については中間の規則を確認してください。

これらの型は「証人（witness）」です。そのいずれかの値を構築するには、その規則に宣言された前提条件を解除（discharge）する必要があります。

仕様からガードタイプへ

shengen

は各規則をターゲット言語内のガードタイプへと降下させます。Go の場合、フィールドは非公開になり、生成されたコンスストラクターがそれらを満たす唯一の手段となります：

type TenantAccess struct {
	principal AuthenticatedPrincipal
	tenant    TenantId
	isMember  bool
}

func NewTenantAccess(principal AuthenticatedPrincipal, tenant TenantId, isMember bool) (TenantAccess, error) {
	if !(isMember == true) {
		return TenantAccess{}, fmt.Errorf("isMember must equal true")
	}
	return TenantAccess{principal: principal, tenant: tenant, isMember: isMember}, nil
}

ここでは奇抜なトリックはなく、単なる通常の Go の可視性です。パッケージ外からのコードはフィールドが小文字であるため

TenantAccess{isMember: true}

を記述することはできません。コンスストラクターだけが値を保持したオブジェクトへの唯一のパスであり、それは

isMember == false

を拒否します。

authenticated-principal

のようなサムの型も同様により、密封されたインターフェースを取得します。生成されたガードを確認してください。

Go はこの投稿全体にわたって例として使用されますが、概念やツールは Go 固有ではありません。Go と TypeScript は現在の生産向けターゲットであり、Python と Rust への参照エmitter もあります。ターゲット言語は実際の選択肢で、実際のトレードオフを持っています：シール（密封）の強度は言語が提供するカプスレーションによって決まり、エージェントもまた言語中立ではありません。

スマートコンスストラクターは古いです。型ラッパーは古いです。コード生成も古いです。有用な動きは、それらをループの一部として配置し、その Enforcement コードよりも短くレビューしやすい仕様から単一の拒否表面（refusal surface）を導き出すことです。

マルチテナントハンドラを書く通常の通りは、各エンドポイントに

if

を置くことです：

if !user.IsMemberOf(tenantID) {
    http.Error(w, "forbidden", http.StatusForbidden)
    return
}

このパターンも理にかなっていますが、まさに第七のハンドラや第三のリファクターで忘れられる種類の「理にかなったこと」です。Shen-Backpressure バージョンではメンバーシップチェックも依然存在します。データベースクエリも存在しますが、それはハンダラー全体に散在する慣習ではなく、

TenantAccess

の構築境界に集中しています：

isMember := exists > 0
access, err := shenguard.NewTenantAccess(principal, tenantID, isMember)
if err != nil {
    return shenguard.TenantAccess{}, fmt.Errorf("tenant access denied: %s is not a member of %s", userID, tenantID.Val())
}

ハンダラーは、すでに通過した連鎖を表現する値に対して動作します。証明はその値と共に移動します。実行中のデモでは、Acme のメンバーである A 氏は Acme リソースのリストを表示できますが、Globex のリソースには拒否されます：

=== Alice requests Globex resources (NOT member - should fail) ===
tenant access denied: user u-alice is not a member of tenant t-globex

エージェントがこの連鎖をスキップして生値（raw value）を渡そうとする場合、バイナリが存在する前にビルドが失敗します：

cannot use tenantID (variable of type string) as shenguard.TenantId value
    in argument to CheckTenantAccess: string does not implement
    shenguard.TenantId (missing method Val)

その短い機械的な「いいえ」こそがバックスプレッシャーです。私はこれらをもっと多く、プロンプトの段落はもっと少なく欲しいです。

やってみましょう

デモは最初から最後まで読むことを意図して構築されています。リポジトリをクローンして

examples/multi-tenant-api/

を開くと、仕様、生成されたガード、そのループを構築した Ralph ループ（

cmd/ralph/

）、そして

demo.md

の cURL スクリプトが含まれています。

これを自分のプロジェクトに接続するには、

sb

CLI をインストールして実行します：

sb init    # 仕様に core.shen + ゲートスクリプトをスケルフトする、
           # .claude/sb ループに /sb:* コマンドをインストールする、
           # ゲート駆動によるバックスプレッシャーを持つ Ralph ループを実行する

sb init

は起動用の仕様とゲートスクリプトをスケルフトし、

-config

を指定すると

sb.toml

マニフェストもスケルフトします。ループの各イテレーションは、

sb.toml

で宣言された固定セットのゲートを走査します：

ゲートコマンド	捕捉する事項
`shengen`	Shen 仕様と生成されたガード間のドリフト
`go test ./...`	ランタイム不変条件の失敗および通常の退化
`go build ./...`	型シグネチャの不整合、無効な証明連鎖の使用
`shen tc` + `bin/shen-check.sh`	Shen 仕様の内部一貫性の欠如
`tcb audit` + `bin/shenguard-audit.sh`	生成されたガードコードへの手動編集

これら 5 つがデフォルトセットです。

sb

は、明示的に構成された場合のみ実行される、第六のゲート（

shen-derive

、仕様同等性テスト用）という、まだ実験的なオプションゲートも持っています。ゲートが失敗すると、その失敗は具体的な文脈として次のプロンプトにフィードされます。それがバックスプレッシャーです。あなたが手動でループを驅動したい場合は、イテレーションの間に

sb

ゲートを自分で実行できます。ハネス（harness）はプラグ可能で、デフォルトは Claude Code（

claude -p

）ですが、Cursor や Codex も

RALPH_HARNESS

を設定することで動作します。ゲート 4 は Shen ランタイムを必要とします：

brew tap Shen-Language/homebrew-shen && brew install shen-sbcl

。また、

sb init -lang ts

は TypeScript 用の全ゲートループを接続し、コード生成だけでなく完全に Go と並ぶターゲット言語となります。さらに、

/sb:*

コマンド

sb init

がインストールする

.claude/

には、新しいターゲット言語向けの

shengen

イミッターを生成するための完全なプロンプトである

/sb:create-shengen

も含まれています。

コストと限界

仕様に書き込むことは無償ではありません。どの不変条件をエンコードするかを決め、両に読みやすく投影可能なノテーションで表現し、ジェネレーターとオーディットスクリプトを維持する必要があります。生成されたガードコードは聖なるものであり、手動で編集するとオーディットゲートが拒否します。あなたの信頼すべき計算基盤（trusted computing base）には、Shen 型チェッカー、ジェネレーター、ターゲットコンパイラが含まれます。

これでもバイパスを不可能にすることはできません。ここがターゲット言語のトレードオフが本当に浮き彫りになる場所です。Go の場合、ガードパッケージ内のコードは値を偽造できるかもしれませんし、反射とゼロ値も理論的にはエスケープハッチとして利用可能です。不注意な SQL クエリは、コンスストラクターにそれがあるべきではない

true

を渡すことができます。私の主張は意図的に狭く設定されています：

shengen

を使用して仕様の証明をターゲット言語へ降下させることは、指定された不変条件を偶然にバイパスすることを事実上不可能にし、完全に不可能にすることではありません。形式手法の聴衆にはこれは特筆にも値せず、わりと弱い主張です。しかし、LLM 生成コードを製品化している実行者にとっては非常に高いレバレッジを持つツールです。今では、忘れられたチェック、リークしたテナント ID、コピーされて不完全なハンドラーは、偶然に導入することが構造的に難しく高コストとなりました。

仕様自体が間違っていることも、ジェネレーターがドリフトすることも、テストがケースを逃すことも可能です。これらの限界を名指しすることは、ツールを理解し、提供するものを規律を持ってレバレッジするために重要です。

これらゲートをインストールするコスト自体も下がっています：仕様に書くこと、イミッターを書くこと、オーディットスクリプトを書くことは、モデルがずっと上手くなっている作業です。より良いモデルは基盤を不要にしません；それらはそれをスキップすることを正当化しにくくします。

結論（テーゼ）

生産用 AI コディングループにおいては、より良いモデルよりも、より良いバックスプレッシャーが必要です。アティファクトが意図する形状を持っているかどうかを示す決定論的なシグナルが必要なのです。テストは一つのそのようなシグナルを提供し、コンパイラのもう一つ提供し、Shen 仕様に降下したガード型はコンパイラの拒否表面をさらに拡張します——デザイン意図からコードそのものへ移動する証明形状の制約です。

これらはいずれもより良いモデルに対する賭けではありません。しかし能力と確信は異なります。「モデルは信頼できる」というのは書き手についての主張であり、「このアティファクトが不変条件を保持している」は目の前の一つのオブジェクトについての主張です。誰かが、あなたが思いつくすべてのテストを通過する実装をフィーリングコーディング（vibe coding）し得ていても、その実装を書いた人の信頼性（モデルか人間か）はまだ、構造的ゲートがアティファクト自身について何を告げるかには教えてくれません。これが、間違いの道が偶然に取りづらくなっていることがモデル能力のあらゆるレベルで重要である理由です。

そして、あなたがその確信を与える同じゲートは、それを証明するアティファクトもあなたに与えます。「私たちは有能なモデルを使った」ということは規制官や監査人に渡すことができませんが、仕様が、通過したゲート、および緑の CI ラン（CI の実行完了）は渡せるものです。