AI 编码循环验证关卡：结构背压比智能代理更优，Shen-Backpressure 来助力！

结构背压优于智能代理用 Shen-Backpressure 为 AI 编码循环设验证关卡2026 年 5 月 18 日一些最严重的软件漏洞往往不起眼访问控制漏洞仍是 [OWASP 十大安全风险中的头号问题](https://owasp.org/Top10/2025/A01_2025-Broken_Access_Control/)。这些漏洞出现是因为规则被放在系统错误位置当 AI 生成大部分代码时原本脆弱的假设彻底失效。采用另一种方法对于广泛的生产软件而言结构背压比提升代理智能的渐进式改进更有效。现有的模型几乎能编写所有代码限制因素在于能否确定它们实现了想要的功能这种确定性来自编写代码所依赖的基础而非等待更智能的模型。[Shen-Backpressure](https://github.com/pyrex41/Shen-Backpressure) 是为验证这一观点而构建的工具和方法。将通过演示展示其功能然后说明如何将同样的循环应用到自己的项目中。行为关卡与结构关卡大多数提示级别的约束属于“行为关卡”模型通常会遵循指令但也常出错导致流程不稳定。行为关卡依赖模型记住规则、识别适用场景、抵抗局部上下文影响还依赖人类评审人员维护相同的不变规则。“结构关卡”不同编译器、类型检查器等会针对代码产物给出明确答案。这种拒绝能将工作从模型的指令空间转移到模型构建所依赖的基础上。通过编排代码使规则难以被意外违反找出关心的属性以机器可检查的形式表达投影到实现中让循环不断尝试直到生成的代码产物满足规则。这就是 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) 将规则以机器可投影到基础的形式编写出来代码生成器 (shengen) 会将其转换为目标语言中的防护类型。编写 Go 或 TypeScript 代码的模型无需知道 Shen 的存在只需代码能编译通过、关卡能通过即可。多租户身份验证的证明链以下是 [多租户 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;)横线上面的前提条件必须满足才能构建横线下面的结论。完整的链条是 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 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 租户的 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 会搭建一个初始规范和关卡脚本使用 -config 参数还可以搭建 sb.toml 清单。循环的每次迭代都会运行一组固定的关卡这些关卡在 sb.toml 中声明关卡命令检查内容shengensb genShen 规范与生成的防护代码之间的差异testgo test ./...运行时不变规则失败和常规回归问题buildgo build ./...类型签名不匹配、无效的证明链使用shen tcbin/shen-check.shShen 规范内部的不一致性tcb auditbin/shenguard-audit.sh对生成的防护代码的手动编辑这五个是默认的关卡。sb 还有一个可选的、仍处于实验阶段的第六个关卡 (shen-derive用于规范等价性测试)只有在明确配置时才会运行。当某个关卡失败时失败信息会作为具体上下文反馈到下一个提示中这就是背压。如果想手动驱动循环可以在迭代之间自行运行 sb gates。该工具是可插拔的默认使用 Claude Code (claude -p)通过设置 RALPH_HARNESS 也可以使用 Cursor、Codex 等。关卡 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 将规范证明转换为目标语言使得指定的不变规则在实际中“几乎不可能”被意外绕过但并非绝对无法绕过。对于形式方法领域的人来说这可能并不稀奇是一个比较弱的主张。但对于使用大语言模型生成代码的开发者来说这是一个非常高效的工具。现在遗忘的检查、泄露的租户 ID 以及复制但不完整的处理程序等问题在结构上变得难以意外引入代价也更高。规范本身可能存在错误生成器可能会出现偏差测试也可能会遗漏一些情况。明确这些限制对于理解该工具并合理利用其优势至关重要。安装这些关卡的成本正在降低因为模型在编写规范、发射器和审计脚本方面的能力不断提高。更好的模型并不会使基础变得不必要反而会让跳过它变得更难以接受。核心观点对于生产环境中的 AI 编码循环更需要“更好的背压”而不是更强大的模型。需要确定性的信号来告诉你代码产物是否符合预期。测试和编译器能提供这样的信号而将 Shen 规范转换为防护类型则进一步扩展了编译器的拒绝范围提供了从设计意图到代码本身的证明式约束。这并非是对更强大模型的否定。能力和确定性是不同的概念。“模型可靠”是关于编写者的论断而“这个代码产物遵循了不变规则”是关于眼前这个对象的论断。无论是模型还是人类编写者的可靠性都无法像结构关卡那样告诉你代码产物本身的情况。这就是为什么在模型能力的各个层面让错误路径在结构上难以意外选择都很重要。同样能给你带来确定性的关卡也能为你提供展示这种确定性的代码产物。“我们使用了强大的模型”无法向监管机构或审计人员证明什么但一个规范、通过的关卡和绿色的持续集成运行结果则可以。项目[Shen-Backpressure 自主编码循环的演绎关卡](/projects/shen-backpressure/)关注[RSS 订阅](/rss.xml)[X (reubbr)](https://x.com/reubbr);; (C) 2026 reuben brooks * 纯文本、纯链接、完整订阅源[rss](/rss.xml) [x](https://x.com/reubbr)