让 AI 改一个游戏规则，它可能顺手埋下漏洞：代码能跑，却不一定守规矩。Bend 想给这种代码加一道“硬门禁”。开发者先在 LAWS.bend 写下程序绝不能违反的规则，再要求 AI 提交实现和证明；形式化证明，就是把规则写成数学命题，让机器检查代码是否必然满足它。
官网演示中，用户让 Claude 把棋盘改成环绕式：没有规则文件时，错误直接进入程序；加入“任何移动序列都不能获胜”这条规则后，AI 必须重试，直到实现通过证明检查。Bend 的类型检查器受 Lean 和 Rocq 一类证明工具启发，但并非直接调用 Lean。项目方称，检查最多约一秒，适合 AI 每次修改后运行；语言还可编译成本地代码，并把并行任务交给多核 CPU 或 GPU，单核运行速度接近 C、GPU 最快可达单核百倍。上述性能和“错误无法合并”的效果均为项目方自述；Bend 仍在快速演进，官网也提醒可能存在缺陷。