形式化验证3D CSG：信任93行规约而非千行AI代码

当AI生成代码，我们该信任什么？

随着AI编程助手的普及，开发者越来越多地依赖大模型生成代码。但一个尖锐的问题随之浮现：当AI一口气生成上千行代码时，我们如何确信这些代码是正确的？

近日，一个名为「形式化验证3D CSG」的项目登上了Hacker News（获得37分、14条评论），提出了一个极具启发性的答案：与其审查1000行AI生成的代码，不如信任93行经过形式化验证的规约（specification）。

形式化验证3D CSG项目

这个项目聚焦于3D CSG（Constructive Solid Geometry，构造实体几何），这是一种通过布尔运算（并集、交集、差集）组合简单几何体来构建复杂三维模型的技术，广泛应用于CAD建模、3D打印和游戏引擎中。

CSG是计算机图形学和CAD领域的基础建模技术，其核心思想源于集合论。开发者可以从球体、立方体、圆柱体等基本几何原语出发，通过布尔运算构建任意复杂的三维模型。例如，要建模一个带孔的金属块，只需将一个立方体与一个圆柱体做差集运算。CSG在工业界的应用非常广泛：OpenSCAD等开源CAD工具以CSG为核心建模范式，Unity和Unreal等游戏引擎用CSG进行关卡原型设计，3D打印领域则依赖CSG进行模型的布尔合并与切割。然而，CSG的实现极其复杂——浮点精度问题、退化几何（如共面三角形）、边界情况处理等都使得正确实现CSG成为计算几何领域的经典难题。正是这种「概念简单但实现困难」的特质，使它成为形式化验证的理想试验场。

核心思路：让形式化规约成为信任的锚点

什么是形式化验证

形式化验证（Formal Verification）是一种基于数学证明的方法，用于严格证明程序的行为符合其规约。与传统的软件测试不同，测试只能证明「在特定输入下没有发现bug」，而形式化验证能够从数学上证明程序对所有可能的输入都满足给定的性质。

形式化验证并非新概念，其历史可追溯到上世纪60年代Tony Hoare提出的Hoare逻辑。当前主流的形式化验证工具包括：Coq（基于构造性类型论的交互式定理证明器）、Lean（微软资助开发的新一代定理证明器）、Isabelle/HOL（基于高阶逻辑的证明助手）、以及TLA+（Leslie Lamport设计的用于并发系统规约的语言）。在工业界，形式化验证已有成功案例：Intel使用形式化方法验证芯片设计以避免类似Pentium FDIV那样的浮点错误，Amazon Web Services使用TLA+验证分布式系统协议，CompCert项目则提供了经过Coq完全验证的C编译器。这些案例证明形式化验证不仅是学术研究，更是工程实践中保障关键系统正确性的有力工具。

这个项目的精妙之处在于抓住了信任问题的本质：无论代码是人写的还是AI生成的，真正需要人类去审查和信任的，应该是那份定义「正确性」的规约，而非具体的实现细节。

93行规约 vs 1000行AI代码的博弈

项目标题本身就是一个鲜明的价值主张。让我们拆解这背后的逻辑：

1000行AI代码：实现复杂、难以逐行审查，AI可能引入难以察觉的边界情况错误。人类review千行代码不仅耗时，而且极易遗漏问题。
93行规约：高度浓缩地描述了「CSG运算应该满足什么性质」。这份规约足够简短，人类可以完整理解并确信它正确表达了意图。

一旦规约被人类信任，形式化验证工具就能自动证明那1000行实现确实满足这93行规约。于是，信任被优雅地转移到了一个人类可以掌控的规模上。

「规约与实现分离」的思想在计算机科学中有着深厚的理论根基。Dijkstra在其经典著作《A Discipline of Programming》中就强调，程序的正确性应当相对于其规约来定义。这一思想在契约式设计（Design by Contract，由Bertrand Meyer在Eiffel语言中推广）、依赖类型（Dependent Types）、以及精化类型（Refinement Types）等技术中都有体现。规约本质上回答的是「What」（系统应做什么），而实现回答的是「How」（系统如何做到）。在AI编程时代，这种分离获得了新的实践意义：当实现成本趋近于零（由AI完成），人类的核心价值就聚焦于精确表达意图——即编写正确的规约。

为什么形式化验证在AI编程时代格外重要

AI代码的信任危机

当前的AI编程范式下，开发者面临一个悖论：AI能快速产出大量代码，但代码量的膨胀反而加剧了审查负担。传统的「人工code review」在面对海量AI生成代码时，逐渐失去了可行性。

当前主流的AI编程助手（如GitHub Copilot、Cursor、Claude等）基于大语言模型（LLM），其代码生成本质上是概率性的token预测过程，而非逻辑推理。多项研究表明，AI生成代码的正确率因任务复杂度而异：在简单的算法题上可能达到80%以上，但在涉及复杂状态管理、并发控制或边界条件处理的场景中，正确率可能显著下降。更棘手的是，AI生成的错误往往具有「表面合理性」——代码结构完整、命名规范、甚至能通过部分测试用例，但在特定边界条件下会产生错误结果。这种「看起来对但实际有微妙bug」的特性，使得人工审查变得尤为困难。

这个项目提出的方案指向了一条可能的出路：将信任的对象从「实现」转移到「规约」。规约本质上是意图的形式化表达，它天然比实现更简洁、更接近人类的思维方式。

从「审查代码」到「审查意图」

这一转变的意义深远。在传统软件工程中，规约往往是模糊的、写在文档里的、与代码脱节的。而形式化验证要求规约必须精确、可执行、且与实现严格绑定。

当AI承担了大部分实现工作后，人类的角色可以聚焦于：

编写和审查规约——确保我们真正想要的东西被正确定义
信任验证工具——让数学证明取代人工逐行检查
专注于高层设计——把精力投入到「做什么」而非「怎么做」

这实际上重新划分了人类与AI在软件开发中的职责边界。

3D CSG作为形式化验证对象的合理性

选择3D CSG（构造实体几何）作为形式化验证的对象颇具智慧。CSG运算有着清晰的数学定义——布尔集合运算，其正确性可以用几何和集合论的语言精确描述。

这类问题恰恰是形式化验证的理想场景：

数学基础扎实：并集、交集、差集都有明确的数学语义
性质易于表达：如运算的交换律、结合律、边界处理等都可形式化
实现复杂但规约简单：几何计算的代码往往冗长且充满边界情况，而其应满足的性质却相对简洁

这种「规约简单、实现复杂」的特性，正是形式化验证发挥最大价值的地方，也完美契合了「93行规约 vs 1000行实现」的对比。

对未来软件开发的启示

验证优先：一种可扩展的信任模型

这个项目虽小，却勾勒出一种在AI时代仍然可靠的信任模型。随着代码生成能力的持续增强，「验证优先」的开发范式可能会变得越来越重要。

试想一个未来：开发者只需精心编写正确的规约，AI负责生成满足规约的实现，形式化验证工具则自动保证二者一致。人类无需再阅读那些机器生成的实现细节，只需确信自己的意图被准确捕捉。

「验证优先」（Verification-First）的理念正在获得越来越多的关注。在区块链和智能合约领域，由于代码一旦部署就不可更改且直接管理资产，形式化验证已成为行业最佳实践——Certora、Runtime Verification等公司专门提供智能合约的形式化验证服务。在AI辅助编程领域，新兴的研究方向包括：让AI不仅生成代码还生成证明（如AlphaProof在数学竞赛中的尝试）、基于规约的代码合成（Program Synthesis）、以及利用LLM辅助编写形式化规约。这些趋势表明，形式化方法与AI的融合正在从学术研究走向工程实践，有望在未来形成一种新的软件开发范式。

现实的挑战与局限

当然，这条路径也面临现实挑战。形式化验证本身有较高的门槛，编写正确的规约需要专业技能，而且并非所有软件问题都像CSG这样有清晰的数学定义。对于业务逻辑复杂、规约本身就难以形式化的应用，这套方法的适用性仍有待探索。

此外，验证工具的能力边界、性能开销、以及规约本身可能存在的错误（garbage in, garbage out），都是需要审慎对待的问题。值得注意的是，形式化验证领域存在一个被称为「验证者的困境」的问题：验证工具本身的正确性如何保证？主流的应对策略包括使用经过验证的证明检查器（如Coq的内核仅有数千行代码，足够小到可以被人工审计）以及多工具交叉验证。这些都是在实际推广「验证优先」范式时需要直面的工程现实。

结语

这个登上Hacker News的小项目，用一个巧妙的对比揭示了AI编程时代的核心命题：在代码可以被无限生成的世界里，信任的稀缺资源是「正确性的证明」，而非「代码本身」。

93行规约与1000行实现的对照，不只是一个技术demo，更是一种开发哲学的宣言——把人类的信任锚定在可掌控、可验证的规约之上，让机器去承担繁重的实现与证明。这或许正是形式化方法与AI编程走向融合的一个缩影。