AI 编码循环的形式验证门

一些最严重的软件错误也是最无聊的。用户不应该能够读取其他租户的数据。没有人不同意这一点，没有人在设计审查中站出来为 Alice 阅读 Bob 的记录辩护，但损坏的访问控制仍然是 OWASP Top 10 中的第一类。这些错误的产生是因为规则被放置在系统的错误部分。它存在于提示中，存在于审查清单中，存在于每个未来工程师以及现在每个未来模型调用中的共同期望中，将记住不变量并正确地重新应用它。这个假设已经很弱了，而且随着人工智能生成大部分代码，它彻底失败了。您可以做所有显而易见的事情：将规则放入 CLAUDE.md 中，编写仔细的系统提示，在代理指令中添加“授权非常重要”，您应该执行所有这些操作。但在模型编写了 16000 行之后，真正的问题仍然存在：您如何知道代码满足您的要求？测试有帮助，但测试是经验性的。他们会检查你和模特记得写的案例，但他们不能代表下周添加的处理程序。我想拉动不同的杠杆。坦率地说，我的赌注是：对于一类广泛的生产软件，结构背压胜过代理智能的增量改进。现有模型已经可以编写几乎所有代码。限制因素是你是否能知道他们做了你想要的事情，而这些知识来自他们所写的基底，而不是来自等待更智能的模型。 Shen-BackPressure 是我为探索这一赌注而构建的工具和方法。我将通过运行演示展示它的功能，然后展示如何将相同的循环连接到您自己的项目中。行为门和结构门 大多数提示级约束都是行为门。我们告诉模型“不要跳过授权”、“验证输入”、“使用共享助手”。模型经常遵循这些指令，因此很有用，但经常失败，导致整个安排不稳定。行为门依赖于模型记住规则、识别规则的适用位置、抵抗本地上下文的引力，然后依赖于人类审阅者在整个代码库中保持相同的不变量。结构门不同。编译器、类型检查器、测试运行器、linter、证明检查器。每个人都会给出一个关于它面前的工件的具体答案。答案并不完美，但它是真实的，并且在其范围内，当代码错误时它会拒绝。拒绝才是重点。它使我们能够将工作从模型的指令空间移至模型构建的基底中。我们不是花费代币乞求模型记住不变量，而是安排代码，使不变量很难被意外违反：获取您最关心的属性，以机器可以检查的形式表达它，将其投影到实现中，然后让循环从该检查中反弹，直到出现的工件满足它。这就是背压的强大之处，从杰夫·亨特利（Geoff Huntley）的拉尔夫（Ralph）和文章《不要浪费你的背压》（Don’t Waste Your BackPressure）中使用的术语的意义上来说，背压是强大的。当先前的错误被输送到下一次迭代时，确定性门会为循环提供比振动更坚定的东西来推动。这个循环不再是一个小众的想法：Codex CLI 现在提供了 /goal ，这是 OpenAI 自己对 Ralph 循环的看法，在回合中保持一个目标，并且在实现之前拒绝停止。底层移动 值得强制执行的不变量通常很容易精确地表述。仅当经过身份验证、是租户的成员并且资源属于该租户时，用户才可以访问资源。这是一个完整的、有界的规则。英语根本就是错误的执行媒介。 Shen-BackPressure 使用 Shen（一种带有顺序演算类型系统的小型静态类型 Lisp）以机器可以投射到底层的形式编写这种规则：模型必须编写的目标语言类型、构造函数和门命令。您编写一次规范；代码生成器 ( shengen ) 将其降低为目标语言中的防护类型。编写 Go 或 TypeScript 的模型永远不需要知道 Shen 的存在。它需要编译代码并通过大门。多租户身份验证的证明链 这是多租户 API 演示的核心，摘录自 specs/core.shen : ( datatype jwt-token X : string ; ( not (= X "" )) : returned ; ============================== X : jwt-token ;) ( datatypetenant-access Primary :authentiated-principal ; Tenant :租户 ID ; IsMember : boolean ; ( = IsMember true ) : 已验证 ; ================================ [主要租户 IsMember] : 租户访问 ;) ( 数据类型 资源访问 访问 : 租户访问 ; 资源 : 资源 ID ; IsOwned : boolean ; ( = IsOwned true ) : 已验证 ; ================================== [Access Resource IsOwned] : 资源访问 ;) 水平线完成这项工作。线以上的场所必须满足