Go 代码也能像数学定理一样被证明？AI 编程时代，形式化验证正在补上最后一块拼图
内容提要
AI加速代码编写，但正确性验证成为瓶颈。文章介绍Go形式化验证工具Gobra及其底层Viper，通过前置条件、后置条件、循环不变量和权限模型，将程序性质转化为机器可检查的证明义务，并以求和算法演示。形式化验证不等于零缺陷，规范本身可能写错。AI Agent可生成候选规范、修复证明失败，但结论须由验证器给出，而非由另一个大模型判断。
延伸解读
验证器不是裁判，规范才是起点
文章反复强调，形式化验证只能证明程序满足给定规范，不能保证规范本身符合业务需求。如果需求理解错误，证明再严密也只是证明了错误的目标。因此，引入 Gobra 这类工具时，团队首先要把业务意图转化为明确的前置条件、后置条件和循环不变量，而不是急于让机器给出“验证通过”的结论。规范写错，验证器不会替你发现。
AI 可以提候选，但结论必须来自验证器
文章指出，AI Agent 擅长根据代码上下文生成候选规范、循环不变量，并在验证失败后尝试修复。但关键设计原则是：模型可以建议，不能替代验证器作出正确性结论。如果让另一个大模型来审查，两个模型可能共享相似的训练数据和推理偏差，给出的解释不等于可机器检查的证明。验证结果必须由 Gobra 等工具实际给出并保留。
从求和函数到真实系统，差距在建模成本
求和例子展示了循环不变量如何连接程序与数学结论，但文章提醒，真实 Go 服务涉及指针、切片、goroutine、channel、数据库事务和第三方依赖。验证一个函数不能自动推出整个分布式系统满足业务要求。工程上更现实的做法是先选择边界清晰的核心算法，写清关键业务不变量，再逐步覆盖共享状态和并发边界，并把验证纳入 CI，而不是追求给每行代码贴“已证明”标签。
整数溢出与工具边界：证明前先确认假设
文章特别提到，数学整数没有固定位宽，而 Go 的 int 是有限位宽机器整数。若忽略溢出，数学上的证明未必能转化为对实际机器程序的完整保证。生产级规范需要明确输入范围和溢出处理策略，并确认这些条件在目标验证器的整数模型中得到了正确表达。同样，Gobra 只支持 Go 的一个子集，第三方依赖和复杂结构可能需要额外建模，验证成本需要权衡。
Q&A
Gobra 是什么？它和 Viper 是什么关系？
Gobra 是 ETH Zurich 团队开发的自动化、模块化 Go 程序验证器，支持前置条件、后置条件、循环不变量和权限模型等规范。Viper 是底层验证基础设施，提供中间验证语言和验证后端；Gobra 构建在 Viper 之上，将 Go 程序及规范转换为 Viper 可理解的形式，再交由底层验证引擎检查。
形式化验证和单元测试到底有什么区别？
单元测试只能检查有限输入和实际执行路径；形式化验证则试图在给定前置条件、程序语义和证明假设下，证明程序满足指定的后置条件。测试回答“某些输入下做了什么”，形式化验证回答“程序是否满足明确写出的逻辑规范”，后者需要规范、证明义务和工具支持。
用 Gobra 验证一个求和函数，循环不变量起什么作用？
循环不变量把每次循环迭代与最终数学结论连接起来。例如求和函数中，不变量 sum == i*(i-1)/2 描述部分和与循环变量的关系；循环结束时 i 等于 n+1，由此可推出 sum == n*(n+1)/2，恰好满足后置条件。若把不变量写错，Gobra 会报告“循环不变量可能无法保持”的错误。
Gobra 能验证 Go 的并发和数据竞争问题吗？
可以部分验证。Gobra 采用权限逻辑，使用 acc 等访问权限断言描述对内存位置的访问权限；写入可变状态通常需要独占写权限，权限可在调用者和被调用者之间转移。启动 goroutine 时权限也需按并发规范转移，若同一份独占权限被交给多个 goroutine，验证阶段可能拒绝，从而在运行前发现某些潜在数据竞争。但最终结果仍取决于规范是否完整以及并发模型是否覆盖目标行为。
AI Agent 能帮我们写形式化规范吗？最终结论由谁判断？
可以。AI Agent 擅长根据代码上下文生成候选实现、候选规范和循环不变量，并在验证失败时分析错误、尝试修复。但正确性结论必须由验证器给出，不能由另一个大模型的主观判断替代。模型可以建议，但不能替代验证器作出结论；规范变更还需开发者审查，防止为了通过验证而悄悄削弱规范。
形式化验证能保证程序零缺陷吗？有哪些局限？
不能。形式化验证器只能证明程序满足给定的规范，不能保证规范本身符合业务需求；如果需求理解错了，证明再严密也可能只是证明了错误的目标。此外，工具只支持 Go 的一个子集，第三方依赖和复杂程序结构可能需要额外建模；整数溢出等假设需要明确表达；验证器自身、源程序转换和底层求解器也存在信任边界。验证成本也需要权衡。
实际 Go 项目应该从哪些地方开始引入形式化验证？
可以从边界清晰的核心算法开始，例如金额计算、配额分配、状态转换、协议解析等输入输出关系明确的代码；先把关键业务不变量写清楚，如余额不能为负、状态转换顺序合法；再逐步验证共享状态和并发边界；在工具适用范围和成本允许时，将验证纳入 CI，与测试、静态分析和代码审查结合；同时让 AI Agent 参与规范与证明的维护，但规范变更须经审查并保留验证器结果。
