AI にコードを書かせるとき、「もっと賢くなれ」より「間違えにくい土台を作れ」のほうが効く、という主張です。
これ、かなり筋がいいと思います。というのも、AI の性能をいくら上げても、最後に壊れるのはたいてい「うっかり忘れた権限チェック」みたいな地味な部分だからです。地味だけど、事故るとめちゃくちゃ痛い。そこを prompt の気合いで守るのは、正直かなり心もとないです。
元記事の冒頭は、かなり本質的です。
「あるユーザーが別の tenant のデータを読めてはいけない」
誰も反対しない、超当たり前のルールです。なのに、broken access control は OWASP Top 10 の常連。
つまり、みんな分かっているのに、実装で漏れるんですよね。
理由はシンプルで、こういうルールが
みたいな、忘れやすい場所に置かれているからです。
AI がコードの大半を書く時代になると、この問題はもっと厄介になります。人間が「次の担当者に引き継ぐ」感覚で守っていた invariant（不変条件）が、モデルの生成のたびに再実行されるからです。
ここでいう invariant は、たとえば「この resource は、その tenant の member だけが見られる」みたいな、破ってはいけないルールのことです。
記事の中心には、かなり強い仮説があります。
多くの production software では、エージェントを少し賢くするより、構造的な backpressure のほうが効く
backpressure は本来、流れてきたものに対して「これ以上は無理」と押し返す仕組みのことです。
この記事では、AI の生成ループに対して、機械がちゃんと拒否する gate を置くイメージで使っています。
つまり、
よりも、
のような、コードが間違っていたら機械が通さない仕組みに寄せたほうが強い、という話です。
これはかなり納得感があります。
人間やAIの「覚えておく」は、結局ふわっとしているんですよね。でも compiler はふわっとしていない。そこが強い。
記事では、これを2種類に分けています。
これは「振る舞いをお願いする」タイプです。
こういう指示は有効ですが、モデルが思い出すかどうかに依存します。
つまり、うまくいくときはうまくいくけど、長いコードや複雑な変更で崩れやすい。
こちらは、構造そのものが間違いを弾くタイプです。
この手の gate は、「ダメなものはダメ」とはっきり言います。
記事が面白いのは、ここを AI へのお説教ではなく、土台の設計問題として扱っているところです。
個人的には、ここが一番重要だと思います。AI を育てるより、AI が踏む床を固くするほうが、実務ではずっと効くことが多いからです。
記事では、Shen-Backpressure というツール／手法が紹介されています。
Shen は、小さな statically-typed Lisp で、sequent-calculus type system を持つ言語だと説明されています。
ここで重要なのは、Shen 自体が主役というより、spec を書いて、それを target language の guard に落とすという流れです。
ざっくり言うと：
つまり、AI に「正しく書いてね」と頼むのではなく、正しくない書き方をしにくくするわけです。
この発想、かなり好きです。人間の根性に期待しない設計は、だいたい強い。
元記事のデモは、multi-tenant API の権限制御です。
multi-tenant というのは、1つのシステムを複数の顧客組織（tenant）が共有する形のこと。たとえば、A社のデータをB社が見られないようにする必要があります。
ここで記事は、認証を次の鎖として表します。
つまり、最終的に resource に触れるには、
という順番を踏む必要がある、ということです。
Shen の仕様では、横線の上が前提、下が結論です。
これは論理学や証明の書き方に近くて、前提を満たさないと結論を作れないという意味を持ちます。
ここはかなり美しいです。
権限チェックを if 文の集合としてではなく、証明オブジェクトの生成条件として扱っているからです。
記事で出てくる witness（証人）という考え方も面白いです。
ある型の値を作るには、その値が正しいことを示す前提を満たしていないといけない、という発想です。
つまり、単なるデータではなく、
という証明を、値そのものにくっつける感じです。
こうなると、handler 側は「毎回チェックする」よりも、「すでに証明済みの値を受け取る」形になります。
これ、実装の重心がかなり変わります。ミスが散らばらず、境界に寄るのが良いですね。
元記事では、Shen の spec から Go の guard type が生成される例が示されています。
たとえば TenantAccess は、フィールドが unexported になっていて、外から勝手に組み立てられません。
ポイントはここです。
isMember == true をチェックするこうすると、外部コードは TenantAccess{isMember: true} のような不正な作り方ができません。
Go の通常の可視性ルールを使って、「勝手に偽装できない」形にしているわけです。
これは派手ではないけれど、実務ではかなり効きます。
「テクニックとして新しい」というより、「当たり前の制約を、ちゃんと中央集権化した」感じです。こういうの、地味だけど強い。
通常の実装では、各 endpoint にこんな if が散らばります。
if !user.IsMemberOf(tenantID) {
http.Error(w, "forbidden", http.StatusForbidden)
return
}
これ自体は悪くないです。
でも、ハンドラが増えたり refactor が入ったりすると、どこかで忘れやすい。
元記事の方式では、membership check は消えません。
ただし、それは handler のあちこちではなく、TenantAccess を作る境界に集約されます。
つまり、handler は「チェックする場所」ではなく、「証明済みの値を使う場所」になる。
この分離はきれいですし、ミスの混入経路も減ります。
デモでは、Alice は Acme の member として扱われます。
なので Acme の resource は見られるけれど、Globex の resource は拒否されます。
拒否メッセージは、かなり素直です。
tenant access denied: user u-alice is not a member of tenant t-globex
この「機械的な no」が、記事の言う backpressure です。
変な例外処理や雰囲気レビューではなく、ちゃんと止まる。ここは良い意味で冷たいです。
記事では、AI が証明チェーンを飛ばして raw value を渡そうとすると、binary ができる前に build が失敗すると説明しています。
これはかなり大きいです。
なぜなら、runtime でエラーになるよりも、compile-time で弾けるほうが圧倒的に安全だからです。
要するに、
ではなく、
に寄せているわけです。
これが structural gate の強さです。
元記事のプロジェクトには、以下が含まれます。
cmd/ralph/demo.md の curl transcriptまた、自分のプロジェクトに組み込むための CLI として sb があり、sb init と sb loop を使う流れが紹介されています。
gate は sb.toml に定義され、たとえば次のようなものがあります。
shengen で spec と生成コードのズレを検出go test ./... で runtime の不具合を検出go build ./... で型や proof chain の不整合を検出shen tc+ で Shen spec の内部整合性を検証tcb audit で生成済み guard code の手編集を検出要するに、AI がコードを書き、gate がダメ出しし、その失敗が次の iteration の材料になる、という loop です。
この loop 設計はかなり実践的だと思います。
AI に「直して」と言うだけでなく、直すための反発面を用意しているからです。
元記事もかなり正直で、「これで何でも防げる」とは言っていません。
制約やコストとしては、たとえば：
つまり、完全な防壁ではないです。
でも著者の主張はそこではなく、「意図した invariant を accident に破るのをかなり難しくする」ことにある。
この線引きはすごく大事です。
セキュリティや権限制御で「絶対に不可能」をうたう設計は、だいたいどこかで無理が出ます。だから、実務的に「事故りにくい」へ寄せるのは賢いと思います。
読んでいて感じたのは、この記事は AI coding の話に見えて、実はソフトウェア設計の古典的な話でもある、ということです。
昔から強い設計は、
方向に進んできました。
AI が入ると、この傾向はさらに強くなると思います。
なぜなら、AI は平均的なコードを書くのは得意でも、「この invariant は絶対に落とすな」みたいな長期記憶は苦手だからです。
だからこそ、元記事のメッセージはかなり現実的です。
「もっと賢いモデルを待つ」より、「今あるモデルでも壊せない構造を作る」。この発想は、かなり実戦向きではないかと思います。
元記事は、AI coding loop においては prompt でのお願いより、structural gate による拒否のほうが強い と主張しています。
Shen を使った仕様から Go や TypeScript の guard を生成し、権限チェックや不変条件を型レベル・構造レベルに押し込むことで、AI がうっかり間違える余地を減らす、という話です。
個人的には、これはかなり筋の良いアプローチだと思います。
AI に仕事を任せるほど、「正しく書いてね」より「間違えたら通らない」に寄せるのが大事になる。地味ですが、こういう地味なところに本当の価値があるんですよね。