你让 AI 给游戏加上“地图边缘可以环绕”的功能。它很快交出代码，也可能顺手打开一条本不该存在的获胜路径。人很难逐行审查 AI 生成的大量代码。Bend 2 想换一种办法：先把不可违反的要求写成数学规则，再要求 AI 每次改代码都交一份证明。编译器负责验算，证明不过，修改就不能放行。
这个单日新增 193 星的语言项目，抓住了 AI 编程最棘手的问题：代码生成得越来越快，我们却未必知道它是否真的按要求工作。以下功能与性能说法均来自 bendlang 官方 GitHub 仓库，目前没有第三方评测支撑。
把提示词变成硬约束
Bend 2 引入 LAWS.bend。开发者可以在这个文件里声明应用必须遵守的规则，例如“账户余额总和必须为零”“玩家不能穿墙”，或者“排序函数的结果必须升序”。
这些不是写给 AI 参考的自然语言备注，而是形式化规格——把“程序应该做什么”写成没有歧义、可由机器检查的数学命题。代码修改后，AI 还要在 PROOF.bend 中给出证明。Bend 编译器逐步检查证明是否成立。形式化证明在这里就像一道带验算过程的门禁：答案看起来合理还不够，推导也必须通过。
官方演示设置了一条规则：“获胜不可能。”当 AI 修改地图环绕逻辑时，没有 LAWS.bend，违反这条规则的代码会被合并；启用后，编译器拦下修改，要求 AI 重试。这里被挡住的并非所有意义上的 bug，而是一个明确违反既定规则的行为。
Bend 把这套机制概括为“有证明支撑的 AGENTS.md”。AGENTS.md 通常用于告诉编程智能体该遵守什么；LAWS.bend 更进一步，试图让其中的重要要求可以机械验证。
证明之外，它还想跑得快
Bend 不只想做证明工具，也想成为能直接运行程序的语言。它采用强类型、纯函数和线性类型：类型系统规定哪些数据和操作合法；纯函数不会暗中修改外部状态；线性类型则限制资源如何使用。这些约束让程序更容易推理，但也带来更繁琐的写法。
官方称，Bend 编译器能在不到一秒内检查其他项目需要数分钟处理的证明文件，并把目标定为以多个数量级超过现有证明助手。性能方面，它声称单核执行可达到手写 C 的速度，在数万核心上甚至更快；长期目标则是 CPU 接近 C、GPU 接近 CUDA。它还主张程序员无需手写线程、锁或 GPU kernel——也就是分配显卡具体任务的小程序。示例 pow2(20) 会把计算铺到 4,096 个 GPU 核心。
这些数字展示的是项目野心，不是已经得到独立验证的普遍结论。第一代 Bend 在 2024 年便以自动并行计算受到关注。官方指南当时也承认，编译器生成的机器码“相当糟糕”；Victor Taelin 还表示，在传统数据并行任务上，CUDA 和 Mojo 的原始性能会更强。如今，Bend 把重点转向 AI 代码验证，但“既能证明、又接近 C 和 CUDA”的旧目标仍待兑现。
最值得看的，是它把矛盾摆上了台面
据 Bend GitHub 项目披露，用来检查 AI 代码的 Bend 编译器本身约 99% 由 AI 编写，而且尚未完成全面审计。项目还列出了证明系统可能与 Lean 形式化版本不一致、早期实现可能存在一致性缺陷等风险。于是它成了一个公开实验：AI 写出的验证工具，能否成为另一批 AI 代码的可信裁判？
局限与未知
- 官方所谓“任何能写出来的要求都能成为 law”过于宽泛。自然语言需求未必容易、正确或可能被形式化。
- 证明只能覆盖规格已经表达的性质。规格写错、漏写，或验证工具自身存在缺陷，都不能由证明自动补救；通过检查也不等于代码没有任何 bug。
- 仓库没有给出完整测试条件、可复现实验结果或独立基准，也未提供 Bend 2 的明确发布日期和正式发布公告。项目还很年轻：代码冗长，没有自动证明搜索，递归必须可终止，数字类型和语言功能也相当有限。