Bend 2 与“氛围编程”陷阱：为什么跳过前期研究会导致冗余的形式化验证工作

核心要点

Bend 2 试图让人们编写法则，同时由大语言模型（LLM）生成实现和证明，但这种方法需要 58 行法则规范和 442 行 AI 生成的证明。相比之下，同样的正确性属性可以在 SPARK 中用不到 12 行代码表达并自动验证，这表明忽视前期研究可能会导致产生不必要的复杂解决方案。

Bend 2 声称提供的功能

人工编写的法则：开发者编码高级不变量（例如，“玩家永远不能触碰旗帜”）。
AI 生成的实现：AI 填充游戏逻辑。
AI 生成的证明：AI 同时编写形式化证明，确保实现遵循这些法则。
编译器验证：Bend 编译器检查证明的可靠性。

Bend 主页上的演示包含一个 LAWS.bend 文件（58 行）和一个对应的 PROOF.bend 文件（442 行）。该博客文章的作者认为，这种冗长反映了设计上的缺陷。

“氛围编程”陷阱解析

“氛围编程（Vibe coding）使得人们在还没充分了解问题以至于认识到存在更好的解决方案之前，就已经构建出了一个庞大的系统。”

氛围编程是指在没有先调研现有文献的情况下，仅凭模糊的想法提示 LLM 生成一个完整的系统。当出现以下情况时，就会陷入陷阱：

跳过研究 – 开发者依赖 LLM 的输出，而不是检查该问题是否已被解决。
产生冗余工作 – 最终的系统重复了成熟工具已经提供的功能。
复杂度膨胀 – LLM 必须生成大量的样板代码（例如 442 行的证明），而这些本可以通过现有的自动证明器避免。

具体对比：Bend 2 与 SPARK

博客作者在 SPARK 中重现了 Bend 的演示，这是一种专为形式化验证设计的基于 Ada 的语言。SPARK 版本包括：

用于列、行和游戏状态的类型定义。
一个表达不变量的 Safe 幽灵函数（ghost function）。
一个带有保证安全性保持的后置条件的 Step 过程。
一个带有玩家永远不会获胜的后置条件的 Replay 函数。
一个用于显示游戏的简单驱动程序。

在此代码上运行 gnatprove 得到：

Success: all checks proved (12 checks).

仅生成了十几个验证条件，且不需要手动编写证明脚本。整个正确性论证由底层的 SMT 求解器自动处理。

关键差异

方面	Bend 2	SPARK
规范大小	58 行法则	~30 行 Ada 类型和契约
证明大小	442 行 AI 生成的证明	0 行（自动 SMT 证明）
工具链成熟度	新兴，重度依赖 AI，99% 由 AI 编写的编译器	数十年历史，经审计，与 GNAT 工具链集成
社区支持	小型，主要处于实验阶段	成熟的 Ada/SPARK 社区，丰富的库

Hacker News 上的社区反应

@pu_pe 指出围绕 Bend 作者声誉的讨论，认为争论更多集中在个人而非技术实质上。
@z7 纠正了关于作者不了解形式化验证的说法，指出了作者之前关于该主题的文章。
@captainmuon 认为现有的验证语言语法通常过于繁重，开发者更希望使用熟悉的语言（如 C# 或 JavaScript）并内置契约。
@mentalgear 强调任何 LLM 驱动的项目都应从“先进行前期工作研究”步骤开始，以避免重复造轮子。
@LightMachine 为设计选择辩护，称显式证明是为了性能考虑，且该语言的内核被刻意保持精简。
@simonw 分享了一个个人工作流：在开始项目之前，要求具备搜索能力的 LLM 找出相关的前期成果，这为他节省了时间。
@thomasahle 澄清说 SPARK 的自动证明依赖于 SMT 求解器，它们是暴力破解式的，无法扩展到像 Lean 或 Bend 那样的交互式证明器的表达能力。
@mccoyb 强调 Bend 2 是一个定量类型理论（QTT）系统，它在验证谱系中处于与 Ada/SPARK 不同的位置。

这些评论展示了分歧的观点：一些人认为 Bend 2 是不必要的重复发明，而另一些人则将其视为对不同验证范式的有益探索。

给使用 LLM 的开发者的建议

从文献调研开始 – 在编写代码之前，要求 LLM 列出与您的问题相关的现有工具、语言和库。
确定验证模型 – 决定您需要的是基于 SMT 的自动验证（如 SPARK、Dafny）还是交互式定理证明（如 Coq、Lean、Bend 2）。
衡量节省的工作量 – 将规范和证明的大小与已知的基准进行比较；过多的样板代码可能表明错过了现有的解决方案。
利用社区资源 – 成熟的生态系统提供经过审计的编译器、标准库和工具，从而降低风险。
将 LLM 输出视为草稿 – 审查生成的证明，确保其正确性并符合目标验证框架中的最佳实践习惯。

结论

Bend 2 展示了 AI 增强形式化验证的广阔前景，但其冗长的证明生成过程突显了一个更广泛的“氛围编程”风险：在不了解现有技术水平的情况下构建复杂的系统。通过进行哪怕是简短的前期调研，开发者通常可以用少量的自动验证条件取代数千行 AI 生成的证明，从而节省时间、Token 并减少潜在的 Bug。围绕 Bend 2 的讨论提醒我们，LLM 在提高生产力的同时，也放大了重复解决已解决问题的风险。