AI编码循环的形式化验证门控

# 结构性反压胜过更智能的智能体 来源：https://reubenbrooks.dev/blog/structural-backpressure-beats-smarter-agents 一些最严重的软件缺陷也是最为乏味的。用户不应该能够读取另一个租户的数据。没有人不同意这一点，没有人会在设计评审会上站起来为“Alice读取Bob的记录”辩护，然而，损坏的访问控制仍然是 OWASP Top 10 中的头号类别（https://owasp.org/Top10/2025/A01_2025-Broken_Access_Control/）。 这些缺陷之所以能发布，是因为规则被放在了系统错误的位置。它存在于提示词中、审查清单中、以及共享的预期中——每个未来的工程师，以及现在每个未来的模型调用，都必须记住这个不变量并正确地重新应用它。 这个假设本来就很薄弱，而当 AI 生成大多数代码时，它就直接失效了。你可以做所有显而易见的事情：把规则放进 `CLAUDE.md`，写一个细致的系统提示词，在智能体指令中添加“授权非常重要”，你也应该做所有这些事。但是，当模型已经写了两万行代码后，真正的问题依然存在：你如何*知道*代码做的是你想要的？测试有帮助，但测试是经验性的。它们检查你和模型记得要写的那些情况，并且它们无法为下周某个人添加的处理程序代言。 我想拉一个不同的杠杆。我的赌注，直白地说，是：**对于一大类生产级软件，结构性反压胜过智能体智能的增量改进。** 现有模型已经可以写出你的几乎所有代码。限制因素在于你是否能*知道*它们做了你想要的，而这种知识来自于它们所编写的底层框架，而不是等待一个更智能的模型。 Shen-Backpressure（https://github.com/pyrex41/Shen-Backpressure） 是我为探索这个赌注而构建的工具和方法论。我将通过一个运行中的演示来展示它的功能，然后展示如何将这个循环接入你自己的项目。 ## 行为门与结构门 大多数提示级别的约束都是*行为门*。我们告诉模型“不要跳过授权”、“验证输入”、“使用共享辅助函数”。模型经常足够好地遵守这些指令，从而有用，但也经常失败，使整个安排变得不稳定。行为门依赖于模型记住规则、识别适用场景、抵抗局部语境的引力，然后依赖于人类审查者在整个代码库中维护相同的不变量。 *结构门*则不同。编译器、类型检查器、测试运行器、linter、证明检查器。每一个都会对面前的制品生成一个具体答案。答案并不完美，但它是真实的，并且在它的作用范围内，当代码错误时它会拒绝。 这种拒绝是关键。它允许我们将工作从模型的指令空间转移到模型正在构建的底层框架中。我们不再花费 token 乞求模型记住一个不变量，而是安排代码使得该不变量很难被意外违反：把你最关心的属性拿过来，用机器可以检查的形式表达它，将其投射到实现中，然后让循环在此检查上弹回，直到最终生成的制品满足它。 这就是反压（在 Geoff Huntley 的 Ralph（https://ghuntley.com/ralph/）和文章《Don't Waste Your Backpressure》（https://banay.me/dont-waste-your-backpressure/）使用的意义上）之所以强大的原因。当先前的错误被输入到下一次迭代时，一个确定性的门给循环提供了一个比“感觉”更坚实的东西来对抗。这个循环不再是少数派的想法：Codex CLI 现在内置了 `/goal`（https://simonwillison.net/2026/Apr/30/codex-goals/），这是 OpenAI 自己对 Ralph 循环的解读，它让目标跨回合保持活跃，并在达成之前拒绝停止。 ## 底层框架转移 值得强制执行的不变量通常很容易精确陈述。*用户只有在经过身份验证、是租户的成员、并且资源属于该租户时，才能访问该资源。* 这是一个完整的、有边界的规则。英语只是*强制执行*它的错误媒介。 Shen-Backpressure 使用 Shen（https://shenlanguage.org/），一个小的、静态类型的 Lisp，具有 sequent-calculus 类型系统，以机器可以投射到底层框架中的形式来编写这类规则：模型必须针对的目标语言类型、构造函数和门命令。你编写一次规范；一个代码生成器（`shengen`）将其降级为目标语言中的守卫类型。编写 Go 或 TypeScript 的模型永远不需要知道 Shen 的存在。它只需要代码能编译且门能通过。 终端录制 sb gates：所有五个门通过，然后一个跳过了租户访问检查的植入缺陷使构建门变红，回滚缺陷后运行恢复到 5/5 绿色。 ## 多租户身份验证的证明链 以下是多租户 API 演示（https://github.com/pyrex41/Shen-Backpressure/tree/main/examples/multi-tenant-api）的核心，来自 `specs/core.shen`（https://github.com/pyrex41/Shen-Backpressure/blob/main/examples/multi-tenant-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`。请参阅完整规范（https://github.com/pyrex41/Shen-Backpressure/blob/main/examples/multi-tenant-api/specs/core.shen）以了解中间规则。 这些类型就是见证者。构造它们中的一个值需要满足其规则中声明的前提。 ## 从规范到守卫类型 `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` 这样的和类型也通过同样的方式获得密封接口。请参见生成的守卫（https://github.com/pyrex41/Shen-Backpressure/blob/main/examples/multi-tenant-api/internal/shenguard/guards_gen.go）文件。 Go 是本文中的示例，但概念和工具并不局限于 Go。Go 和 TypeScript 是目前的生产目标，还有针对 Python 和 Rust 的参考发射器。目标语言是一个真正的选择，具有真正的权衡：密封的强度取决于语言给你的封装能力，而且智能体也不是语言中立的（https://lucumr.pocoo.org/2026/2/9/a-language-for-agents/）。 智能构造函数是古老的。类型包装也是古老的。代码生成也是古老的。有用的地方是把它们放在循环中作为一个单一的拒绝表面，其来源是一个比它生成的强制代码更短且更易于审查的规范。 编写多租户处理程序的常规方式是在每个端点中放置一个 `if`： `` if !user.IsMemberOf(tenantID) { http.Error(w, "forbidden", http.StatusForbidden) return} `` 这种模式是合理的，但正是那种会在第七个处理程序或第三次重构中被遗忘的合理事物。在 Shen-Backpressure 版本中，成员检查仍然存在。仍然有数据库查询，但它集中在 `TenantAccess` 的构造边界上，而不是作为约定分散在各个处理程序中： `` isMember := exists > 0access, 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 成员的 Alice 可以列出 Acme 的资源，但在请求 Globex 时被拒绝： `` === Alice requests Globex resources (NOT member - should fail) ===tenant access denied: user u-alice is not a member of tenant t-globex `` 如果智能体试图跳过链并传递一个原始值，构建会在二进制文件存在之前失败： `` 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/`（https://github.com/pyrex41/Shen-Backpressure/tree/main/examples/multi-tenant-api）：它包含了规范、生成的守卫、构建它的 Ralph 循环（`cmd/ralph/`）以及 `demo.md` 中的 curl 记录。 要将其接入你自己的项目，安装 `sb` CLI 并运行： `` sb init # 生成 specs/core.shen + 门脚本， # 将 /sb:* 命令安装到 .claude/sb loop # 运行带有门驱动反压的 Ralph 循环 `` `sb init` 会生成一个 starter 规范和门脚本，使用 `-config` 还会生成 `sb.toml` 清单。循环的每次迭代都会运行一组固定的门，这些门在 `sb.toml` 中声明： 门 | 命令 | 捕获的内容 --- | --- | --- shengen | `sb gen` | Shen 规范与生成的守卫之间的差异 test | `go test ./...` | 运行时不变量的失败和普通回归 build | `go build ./...` | 类型签名不匹配，无效的证明链使用 shen tc+ | `bin/shen-check.sh` | Shen 规范的内部不一致性 tcb audit | `bin/shenguard-audit.sh` | 对生成的守卫代码的手动编辑 这五个是默认集合。`sb` 还有一个可选的、仍处于实验阶段的第六个门（`shen-derive`，用于规范等价性测试），仅在显式配置时运行。当一个门失败时，失败信息会作为具体上下文输入到下一个提示中。这就是反压。如果你想要手动驱动循环，你也可以自己在迭代之间运行 `sb gates`。这个框架是可插拔的：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 init` 安装到 `.claude/` 中的 `/sb:*` 命令包括 `/sb:create-shengen`，这是一个完整的提示，用于为新的目标语言生成一个 `shengen` 发射器。 ## 成本与限制 编写规范不是免费的。你要决定哪些不变量值得编码，用既可读又可投射的表示法表达它们，并维护生成器和审计脚本。生成的守卫代码是神圣的；手动编辑它会导致审计门拒绝。你的可信计算基础现在包括 Shen 类型检查器、生成器和目标编译器。 它并不会让绕过*不可能*。这就是目标语言权衡真正变得明显的地方。在 Go 中，守卫包内部的代码可以伪造值；反射和零值在理论上可以作为逃生舱。一个粗心的 SQL 查询可能会向构造函数传递一个它不应该有的 `true`。我的主张是刻意狭窄的：使用 shengen 将规范证明降级到目标语言中，使得指定的不变量*实际上不可能*被*意外*绕过，而不是在绝对意义上不可能被绕过。对于形式化方法的受众来说，这并不起眼，而且是一个相当弱的声明。但对于一个发布 LLM 生成代码的从业者来说，这是一个极高杠杆的工具。现在，被遗忘的检查、泄露的租户 ID、以及被复制但不完整的处理程序都变成了*在结构上难以且代价高昂*被意外引入的问题。 规范本身可能是错误的，生成器可能发生漂移，测试仍然会遗漏情况。命名这些限制对于理解这个工具、以有纪律的方式利用它提供的东西非常重要。 安装这些门的成本本身也在下降：编写规范、发射器和审计脚本正是模型不断变得更好的工作。更好的模型并不会让底层框架变得不必要；它们只会让跳过它更难合理化。 ## 论点 对于生产级 AI 编码循环，你需要的*更好的反压*比需要更好的模型更多。你需要确定性信号，告诉你制品是否具有你想要的形状。测试给你一个这样的信号，编译器给你另一个，而将 Shen 规范降级为守卫类型则进一步扩展了编译器的拒绝表面——证明形状的约束从设计意图一直传递到代码本身。 这些都不是在反对更好的模型。但是能力和确定性是不同的事情。“模型是可靠的”是关于写作者的声明；“这个制品维持了不变量”是关于你面前的单个对象的声明。有人可以 vibe-code 出一个实现，通过了你想到要写的所有测试，而写它的人（模型或人类）的可靠性仍然不能告诉你结构门告诉你的关于制品本身的东西。这就是为什么错误路径在结构上难以被意外走通，在每一个模型能力水平上都至关重要。 而给你这种确定性的同一个门也给了你用于证明它的制品：“我们使用了一个有能力的模型”这不是你能交给监管机构或审计员的东西，但一个规范、一个通过的门和一个绿色的 CI 运行则是。