Bend 是一种基于这样一个前提构建的编程语言：随着 AI 智能体越来越多地生成软件，人类需要一种方法来验证生成的代码是否正确实现了他们的意图。该语言引入了一种机制，允许开发者声明“法律”——即应用程序绝不可违反的精确、无歧义的规则。例如，开发者可能会声明一条法律，规定特定的游戏状态是无法达到的。当 AI 智能体尝试修改代码时，Bend 编译器充当守门人：除非 AI 还能提供数学证明来证明新代码符合这些法律，否则它将阻止任何违反这些法律的合并操作。
此视觉效果说明了通过声明“法律”来防止不可能的游戏状态的概念。
这张图片展示了 Bend 编译器“法律”旨在防止的 Bug 类型。
此视觉效果展示了通过成功执行数学法律来维护游戏完整性。
Bend 的技术核心是其编译器，它作为一个高速证明检查器运行。虽然像 Lean 或 Rocq 这样的传统证明助手可能需要几分钟来验证中等规模的代码库，但 Bend 的设计目标是在不到一秒的时间内完成这些检查。这种速度允许 AI 智能体在每次增量更改后验证正确性。此外，Bend 旨在提供高性能，编译为在单个 CPU 核心上运行速度几乎与 C 相当的原生代码。它还支持大规模并行处理，允许代码在数千个 GPU 核心上运行，而无需手动管理线程或编写内核，因为该语言会自动处理工作分配。
此图表支持了 Bend 在不到一秒内执行检查的说法，比传统工具快得多。
此图表说明了 Bend 几乎能达到与 C 相当的运行速度以及对大规模 GPU 并行性的支持。
此动画展示了该语言在无需手动管理线程的情况下处理大规模并行能力。
尽管 Bend 承诺提供“无 Bug”的代码，但使用它也涉及特定的权衡和实际障碍。由于该语言需要形式化证明，即使是基础的算术运算也可能要求开发者或 AI 定义基础属性。例如，有用户报告称，由于基础库缺乏完整的序理论，AI 智能体在处理某些算术法律时感到困难，需要 AI 为最大值等基本函数编写结构递归证明。此外，虽然 Bend 为验证意图提供了一个强大的框架，但为高度复杂的系统定义这些“法律”的复杂性，仍然是那些试图摆脱自然语言规范的开发者需要考虑的重要因素。该项目目前处于早期阶段，其缺乏公开的提交历史已被注意到，这是评估其长期开发和可靠性的一个考量点。