Bend推出LAWS.bend：用形式化证明拦截AI错误代码

Bend 引入 LAWS.bend 机制：用形式化证明阻止 AI 写入错误代码

Bend 语言新增了一项名为 LAWS.bend 的功能，目标很明确：让 AI 代理（agent）在修改代码时提供数学证明，而不是仅凭生成的代码本身。

工作方式如下。开发者在项目中编写一个 LAWS.bend 文件，在其中声明"法律"——即代码必须满足的约束。文件一经提交，任何 AI 都无法直接写入一行违反这些法律的代码。官方用一个小游戏演示了这一机制：AI 被要求改写游戏逻辑，如果它的改动会破坏"赢是不可能的"这条规则，系统就会拒绝合并。

在演示中，开发者在编辑器里要求 Claude 修改棋盘逻辑。

对照实验的结果区分明确：没有 LAWS.bend 时，AI 的改动悄悄引入了违反规则的 bug，代码被合并；启用 LAWS.bend 后，AI 的提交被直接封锁，系统强制其重新尝试，直到改动满足法律为止。

核心差别在于：没有 LAWS.bend，bug 只是被生成出来并存活下去；有了 LAWS.bend，AI 必须重新尝试。由于证明的存在，"合并一个 bug"在数学上不可能成立——它被表达为一个定理。

法律本身用 Bend 语言表达，以一个关于棋盘状态的声明为例：

# LAW: no move sequence leads to victory.
law you_cant_win:
  for moves: List<Move>            # any sequence of moves
  board = replay(start(), moves)   # replayed from the start
  is_won(board) == False{}         # never leads to victory

与法律配套的是证明（proof），由 AI 自动生成并随改动提交：

# PROOF: you_cant_win holds.
def Laws.you_cant_win(moves):
  # ... written by the AI

项目方将 LAWS.bend 定位为对 AGENTS.md 一类约定的升级：后者只是写给 AI 的规范文字，依赖模型自觉遵守；而 LAWS.bend 的约束由编译器强制检查。

对该机制的效果存疑的开发者，可以直接试用官方提供的游戏，尝试让 AI 在启用法律的情况下写入一个能获胜的 bug。