AI编程循环的形式验证关卡

行为Gate与结构Gate

大多数prompt级别的约束都是行为gate。我们告诉模型"不要跳过授权"、"验证输入"、"使用共享的helper"。模型足够频繁地遵循这些指令以保证有用性，又足够频繁地失败导致整个安排变得不稳定。行为gate依赖于模型记住规则、识别它应用的位置、抵抗本地context的吸引，随后依赖于人类审查者在整个代码库中维持相同的不变量。

结构gate是不同的。编译器、类型检查器、测试运行器、linter、证明检查器。每一个都对其前面的工件产生一个具体的答案。答案不是完美的，但它是真实的，在其范围内会对错误的代码说不。

那个"不"就是重点。它让我们把工作从模型的指令空间转移到模型正在构建的基质中。与其花费token恳求模型记住一个不变量，我们改为安排代码使得不变量很难被意外打破：取你最在乎的属性，用机器可以检查的形式表达它，将其投影到实现中，让循环在该检查处反弹，直到新兴的工件满足它。

这就是Geoff Huntley的Ralph论文和"不要浪费你的反压"（Don't Waste Your Backpressure）这篇文章中反压（backpressure）的含义所以强大的原因。当前面的错误被送入下一次迭代时，确定性的gate给循环一些比"感觉"更坚实的东西来对抗。那个循环不再是一个小众的想法：Codex CLI现在发布了/goal，这是OpenAI自己对Ralph循环的实现，在多个轮次中保持一个目标活跃，并拒绝停止直到目标被满足。

值得强制的不变量通常很容易精确表述。用户只有在认证通过、是租户成员且资源属于该租户的情况下才能访问资源。这是一个完整的、有界的规则。英语根本不是强制执行它的恰当介质。

Shen-Backpressure使用Shen（一个小型、静态类型的Lisp，具有sequent-calculus类型系统）来以机器可以投影到基质中的形式写下这类规则：目标语言的类型、构造函数和模型必须写入的gate命令。你一次性编写spec；一个代码生成器（shengen）将其降低为目标语言中的guard类型。用Go或TypeScript编写的模型永远不需要知道Shen存在。它只需要代码编译且gate通过。

多租户认证的证明链

这是多租户API演示的核心，一段来自specs/core.shen的摘录：

principle principal : j_token
  principle ⊢ auth_user

auth_user user : principal
  tenant_id ∈ get_membership user
  ⊢ tenant_access

tenant_access ta : auth_user
  get_owner resource = tenant_id ta
  ⊢ resource_access

水平线做了关键工作。线上方的前提必须在线下方的结论能被构造之前满足。要获得resource_access，你需要tenant_access和资源被拥有的证明，要获得tenant_access，你需要经过认证的principal和成员资格证明。完整的链从jwt-token → authenticated-user → tenant-access → resource-access。详见完整的spec了解中间规则。

这些类型是见证。构造其中一个的值需要满足其规则中声明的前提。

从Spec到Guard类型

shengen将每条规则降低为目标语言中的guard类型。在Go中，字段是未导出的，生成的构造函数是填充它们的唯一方式：

type TenantAccess struct {
  tenantID string
  isMember bool
}

func NewTenantAccess(userID, tenantID string) (TenantAccess, error) {
  member, err := db.IsMember(userID, tenantID)
  if err != nil {
    return TenantAccess{}, err
  }
  if !member {
    return TenantAccess{}, errors.New("not a member")
  }
  return TenantAccess{tenantID, member}, nil
}

这里没有花招，只是普通的Go可见性规则。包外的代码不能写TenantAccess{isMember: true}，因为字段是小写的。构造函数是填充值的唯一路径，它拒绝isMember == false。像authenticated-principal这样的Sum类型以同样的方式获得密封接口。见生成的guards。

Go是这篇文章中的例子，但这些概念和工具不是Go特定的。Go和TypeScript是目前的生产目标，还有Python和Rust的参考发射器。目标语言是真实的选择，有真实的权衡：密封的强度只取决于语言提供的封装强度，而agent也不是语言中立的。

智能构造函数很古老。类型包装很古老。代码生成很古老。有用的着力点是把它们放在循环中作为单一的拒绝表面，源自一个比它生成的强制代码更短、更易审查的spec。

无需手写检查的授权

编写多租户处理程序的常规方式是在每个端点中放一个if：

func ListResources(w http.ResponseWriter, r *http.Request) {
  user := r.Context().Value("user").(User)
  tenantID := r.URL.Query().Get("tenant_id")
  
  // 容易遗漏的检查
  if !isMember(user.ID, tenantID) {
    http.Error(w, "forbidden", http.StatusForbidden)
    return
  }
  
  resources, _ := db.GetResources(tenantID)
  json.NewEncoder(w).Encode(resources)
}

这个模式很合理，但也正是那种在第七个处理程序或第三次重构时容易被遗忘的东西。在Shen-Backpressure版本中，成员资格检查仍然存在。数据库查询仍然存在，但它集中在TenantAccess构造的边界处，而不是散布在各个处理程序中作为一种惯例：

func ListResources(w http.ResponseWriter, r *http.Request) {
  user := r.Context().Value("user").(User)
  tenantID := r.URL.Query().Get("tenant_id")
  
  ta, err := NewTenantAccess(user.ID, tenantID)
  if err != nil {
    http.Error(w, "forbidden", http.StatusForbidden)
    return
  }
  
  // ta 代表已验证的链
  resources, _ := db.GetResources(ta.TenantID())
  json.NewEncoder(w).Encode(resources)
}

处理程序随后对代表已遍历链的值进行操作。证明随值传播。在运行的演示中，Alice是Acme的成员，可以列出Acme的资源，但被拒绝访问Globex的：

$ curl -H "Auth: alice" "http://api/resources?tenant=acme"
[{"id": "r1", "tenant": "acme"}, ...]

$ curl -H "Auth: alice" "http://api/resources?tenant=globex"
forbidden

如果agent试图跳过链并传递一个原始值，构建在二进制存在前就会失败：

error: cannot use RawTenant (type struct{ID string}) as type TenantAccess
  in function argument

那个短暂的、机械的"不"就是反压。我想要更多这样的，更少的prompt中的段落。

这个演示是为了完整阅读而设计的。克隆repo并打开examples/multi-tenant-api/：它包含spec、生成的guards、构建它的Ralph循环（cmd/ralph/）和demo.md中的curl事务记录。

要将其接入你自己的项目，安装sb CLI并运行：

sb init

sb init搭建启动spec和gate脚本，加上-config还会搭建sb.toml清单。循环的每个迭代都运行一组固定的gates，在sb.toml中声明：

[[gates]]
name = "shengen"
[[gates]]
name = "compile"
[[gates]]
name = "lint"
[[gates]]
name = "test"
[[gates]]
name = "shen-check"

这五个是默认集合。sb还有一个可选的、仍在试验的第六个gate（shen-derive，用于spec等价性测试），仅在明确配置时运行。当gate失败时，失败作为具体context送入下一个prompt。那就是反压。如果你想手动驱动循环，可以在迭代间自己运行sb gates。这个harness是可插拔的：Claude Code（claude -p）是默认的；Cursor、Codex和其他工具可以通过设置RALPH_HARNESS来工作。Gate 4需要Shen runtime：brew tap Shen-Language/homebrew-shen && brew install shen-sbcl。sb init -lang ts为TypeScript而非仅codegen接入完整的gate循环。它是一个与Go并列的完整目标。sb init安装的/sb:*命令中包括/sb:create-shengen，一个为新目标语言生成shengen发射器的完整prompt。

编写spec不是免费的。你决定哪些不变量值得编码，用既可读又可投影的符号表达它们，维护生成器和审计脚本。生成的guard代码是神圣的；手工编辑它会被审计gate拒绝。你的可信计算基础现在包括Shen类型检查器、生成器和目标编译器。

它不会使绕过变得不可能。这是目标语言权衡真正显现的地方。在Go中，guard包内的代码可能伪造值；反射和零值在理论上可用作逃生舱。一个不谨慎的SQL查询可能给构造函数传一个不应该有的真值。我的主张故意很窄：使用shengen把spec证明降低到目标语言，使指定的不变量几乎不可能被意外绕过，不是分类上不可能被完全绕过。对于形式化方法的听众，这是平凡的，相当薄弱的主张。但对于运送LLM生成代码的实践者来说，这是一个极高杠杆的工具。现在，被遗忘的检查、泄露的租户ID和不完整拷贝的处理程序都变得结构上很难通过意外引入。

spec本身可能有错，生成器可能漂移，测试仍可能遗漏情况。指出这些限制对于理解工具、以纪律的方式利用它所提供的内容至关重要。

安装这些gates的成本本身在下降：编写spec、发射器和审计脚本正是模型不断进步的工作。更好的模型不会使基质变得不必要；它们使跳过基质更难以辩护。

对于生产AI编码循环，你需要更好的反压胜过更好的模型。你需要确定性信号告诉你工件是否具有你想要的形状。测试给你一个这样的信号，编译器给你另一个，而Shen spec降低到guard类型进一步扩展了编译器的拒绝表面——证明形状的约束，从设计意图传播到代码本身。

这不是对更好模型的赌注。但能力和确定性是不同的。"模型是可靠的"是对作者的论断；"这个工件维持不变量"是对你面前的一个具体对象的论断。有人可以凭感觉编写出通过你想到的每个测试的实现，而作者的可靠性——无论是模型还是人——仍然不会告诉你结构gate告诉你的关于工件本身的东西。这就是为什么无论模型处于哪个能力层级，错误的路径在结构上很难被意外踏上。

相同的给你确定性的gate也给你工件去展示它：我们使用了一个有能力的模型"不是你能交给监管者或审计员的东西，但spec、通过的gate和绿色CI运行是。