AI 代码生成工具的普及带来了效率的飞跃，但也引入了新的质量风险。当模型生成数千行代码后，核心问题不再是 "代码能否运行"，而是 "如何确信代码符合预期的不变量"。传统的解决方案依赖提示工程 —— 在系统提示中反复强调安全规则、授权检查的重要性 —— 但这类行为约束本质上是脆弱的。模型可能遗忘规则，可能在复杂上下文中误判适用场景，而人工审查难以在大量生成代码中持续维护这些不变量。
行为门控的局限
当前大多数 AI 编程助手采用行为门控（behavioral gates）策略。开发者通过精心设计的提示词告诉模型 "不要跳过授权验证"、"始终验证输入"、"使用共享辅助函数"。这种方案在简单场景下有效，但存在根本缺陷：它依赖模型在每次调用时记住规则、识别适用场景、抵抗局部上下文的引力，并最终正确应用规则。当代码库增长到数万行，当多个开发者轮流与模型交互，这种基于记忆的约束必然出现疏漏。
更严重的是，测试作为目前最常用的质量门控，本质上是经验性的。测试只能检查你记得编写的用例，无法覆盖未来添加的处理程序。当 LLM 生成的代码绕过测试却违反关键不变量时，问题往往直到生产环境才会暴露。
结构门控：将约束下沉到代码基底
结构门控（structural gates）提供了不同的思路。编译器、类型检查器、测试运行器、证明检查器 —— 这些工具对代码产物给出确定性答案。它们不完美，但在其能力范围内，它们会拒绝错误的代码。这种拒绝能力是关键：它允许我们将工作从模型的指令空间转移到模型正在构建的代码基底中。
与其花费 token 恳求模型记住不变量，不如安排代码结构使得不变量难以被意外违反。具体做法是：将你最关心的属性用机器可检查的形式表达，将其投影到实现中，让生成循环在检查点处反复验证，直到产物满足规范。
这就是结构反压（structural backpressure）的核心思想。当先前迭代的错误被反馈到下一次提示中时，确定性门控为循环提供了比 "感觉" 更坚实的推进阻力。OpenAI 的 Codex CLI 已内置/goal指令，实现了类似的循环机制 —— 保持目标在多次交互中存活，直到达成才停止。
Shen-Backpressure 的技术实现
Shen-Backpressure 项目将这一理念落地为可复用的工具链。其工作流程分为三个层次：
第一层：规范定义。使用 Shen 语言（一种静态类型 Lisp，具备 sequent-calculus 类型系统）编写领域不变量。例如多租户系统的授权规则可以精确表述为："用户仅在已认证、属于目标租户、且资源属于该租户时，方可访问该资源"。这种规范作为specs/core.shen保存在仓库中，是人类编辑的真相来源。
第二层：代码生成。shengen工具将规范降维为目标语言的守卫类型（guard types）。守卫类型具有未导出字段和经过验证的构造函数，使得目标语言的编译器能够强制执行规范声明的每个不变量。模型编写 Go 或 TypeScript 代码时无需了解 Shen 的存在，只需确保代码能通过编译和门控检查。
第三层：门控循环。每次 Ralph 循环迭代必须通过五道门控：
- shengen 门控：从规范重新生成守卫类型，捕获过期类型
- 测试门控：针对再生类型运行测试，捕获运行时不变量违反
- 构建门控：针对再生类型编译，捕获类型签名不匹配
- Shen 类型检查门控：验证规范内部一致性，捕获矛盾规则
- TCB 审计门控：重新运行 shengen，对比输出，拒绝
shenguard/目录中的非预期文件
可选的第六道门控shen-derive针对纯函数，通过采样输入验证实现与规范的等价性。
可落地的工程参数
要在现有项目中引入形式化验证门控，可参考以下实施清单：
项目初始化：
- 运行
sb init生成specs/core.shen、sb.toml、prompts/目录结构 - 在
sb.toml中声明门控拓扑，支持自定义门控列表和并行组
规范编写原则：
- 聚焦跨越边界的数据（I/O、变异、胶水层），使用
shen-guard生成守卫类型 - 纯函数使用
(define ...)块声明规范，shen-derive自动生成表驱动测试 - 复杂不变量拆解为证明链，如
Amount → Transaction → BalanceChecked → SafeTransfer
CI/CD 集成：
- 将
sb gates作为独立步骤加入流水线 - 配置
SHEN环境变量指定 Shen 运行时（推荐shen-sbcl，启动 0.06 秒） - 提交
.sb/discharge_report.json作为审计级验证产物，包含规范哈希、Git 提交、工具版本、逐规则前提表
故障排查：
- 失败门控自动注入 5 秒 Markdown 摘要到提示上下文（
sb context） - 放电报告附带具体反例：用例 ID、规范输出、实现输出、可直接粘贴的
go test -run ...复现命令
从概念到生产
形式化验证门控的价值不在于完全消除错误 —— 没有任何工具能做到这一点 —— 而在于将关键不变量从 "应该记住" 转变为 "无法违反"。在多租户 API 场景中，JWT 到 AuthenticatedUser 到 TenantAccess 到 ResourceAccess 的证明链确保了授权逻辑在编译期即被验证。在支付处理器场景中，余额不变量的证明链防止了资金错误流转。
这种方案与等待更智能的模型形成鲜明对比。现有模型已经能够编写绝大多数生产代码，真正的瓶颈在于如何确信它们确实按照预期编写了代码。这种确信来自代码基底本身，来自那些模型必须编写通过的结构性检查点。
参考来源：
- Reuben Brooks, "Structural Backpressure Beats Smarter Agents", https://reubenbrooks.dev/blog/structural-backpressure-beats-smarter-agents/
- Shen-Backpressure GitHub Repository, https://github.com/pyrex41/Shen-Backpressure
内容声明：本文无广告投放、无付费植入。
如有事实性问题，欢迎发送勘误至 i@hotdrydog.com。