本文永久链接 – https://tonybai.com/2026/10/25/go-formal-verification-gobra-viper-ai

大家好，我是Tony Bai。

【导读】

AI 已经让写代码的成本大幅下降，但代码生成出来，并不意味着它就是正确的。单元测试只能检查有限的输入，代码审查也难以穷尽所有执行路径。有没有办法，让机器不只是判断程序“看起来没问题”，而是依据明确的数学规范，验证程序是否满足我们要求的性质？

数学领域，Lean 等证明助手已经展示了 AI 与机器可检查证明结合的潜力。在软件工程领域，类似的探索也正在推进。对于 Go 开发者来说，一个值得关注的开源项目是 ETH Zurich 团队开发的 Gobra。它基于 Viper 验证基础设施，通过前置条件、后置条件、循环不变量和权限模型，对 Go 程序的功能正确性、内存访问以及并发行为进行形式化验证。

这意味着，AI 负责生成实现与证明线索，验证器负责检查数学义务，而开发者则需要把真正的业务意图说清楚。Go 的形式化验证，可能成为 AI 编程从“生成更多代码”走向“交付可信软件”的重要一步。

【文章要点】

  • AI 生成代码越容易，验证代码是否正确就越重要。
  • 测试、静态分析、模型检查和形式化验证解决的是不同层次的问题，不能混为一谈。
  • Gobra 是 Go 领域值得重点关注的形式化验证工具，Viper 则提供了底层的权限推理与验证基础设施。
  • 通过一个求和算法，理解前置条件、后置条件和循环不变量如何构成机器可检查的正确性证明。
  • 形式化验证并不意味着“零缺陷”：规范可能写错，工具也有适用范围，验证成本需要权衡。
  • AI Agent 可以协助编写规范、生成不变量和修复证明失败，但最终结论应来自验证器，而不是另一个大模型的主观判断。

AI 把代码写得越来越快，谁来证明它没有写错？

过去，软件工程有一个相对稳定的节奏：开发者理解需求，设计架构，编写代码，运行测试，经过代码审查，再将程序交付生产环境。

今天，这个节奏正在被 AI Agent 改写。

给定一个任务，Agent 可以阅读代码库、修改多个文件、补充测试、运行构建、修复报错，最后提交一个看起来完整的 Pull Request。过去需要程序员花费几个小时甚至几天完成的工作，现在可能在几分钟内就能得到初步结果。

但一个问题随之浮现：当代码的生产速度开始超过人类理解、审查和验证代码的速度，软件工程的瓶颈究竟会转移到哪里？

答案很可能是正确性。

AI 可以生成一个实现，也可以为这个实现编写测试，甚至可以再扮演一个审查者，告诉我们代码看起来没有问题。但这些证据并不等价。

生成代码的模型可能误解需求；编写测试的模型可能遗漏边界条件；审查代码的模型也可能与生成代码的模型犯下同一种错误。

如果整个流程仍然依赖模型自己判断自己是否正确，那么我们只是增加了检查环节，并没有真正建立一个独立、可靠的正确性保证机制。

这正是形式化验证重新受到关注的原因。

2026 年 10 月，OpenAI 发布了一批由内部模型生成的数学研究成果，公开目录包含数百篇数学手稿，并为其中一部分提供 Lean 形式化证明。这里需要注意一个细节：公开目录中的成果并非全部已经形式化，形式化覆盖也不等于每项数学主张都已得到独立的专家确认。

但这件事展示了一种很有价值的工作模式：AI 可以探索问题、提出猜想、寻找证明；Lean 则负责检查形式化证明是否符合既定的数学规则。

机器不必相信 AI 的解释。它只需要检查证明本身。

同样的思路，也正在进入软件工程。

Lucas C. Cordeiro 教授在 FATTW 2026 的报告《Formal Verification of LLM-Generated Code》中，讨论了大模型生成代码与形式化验证之间的关系。他强调，AI 擅长提出候选实现、规范和循环不变量，而验证器提供可机器检查的结论。两者并非替代关系，如何建立可靠的协作接口才是重要的研究问题。

这意味着，AI 编程时代可能出现一种新的软件生产模式：

注意，这里有一个不能省略的前提：形式化验证器只能证明程序满足给定的规范，不能替我们保证规范本身符合业务需求。

如果需求理解错了，证明再严密，也可能只是严密地证明了一个错误的目标。

因此，AI 时代的形式化验证并不是让开发者退出软件工程，而是让开发者把更多精力放在需求、规范、架构和风险上，将机械性的证明检查交给机器。

测试、静态分析和形式化验证，到底有什么不同？

在讨论 Go 语言的具体工具之前，需要先厘清一个经常被混淆的问题：测试通过，究竟意味着什么？

假设我们有一个函数，用于计算从 0 到 n 的整数之和。

func Sum(n int) int {
    sum := 0
    for i := 0; i <= n; i++ {
        sum += i
    }
    return sum
}

对于这个函数，我们可能采用几种不同的验证手段。

方法 可以回答的问题 主要局限
单元测试 指定输入下，输出是否符合预期？ 只能覆盖实际执行的输入和路径
随机测试、模糊测试 大量随机输入下，是否能发现异常？ 没有发现错误不代表不存在错误
静态分析 是否存在特定类型的可疑行为？ 受分析规则与能力范围限制
模型检查 在给定模型、边界或状态空间内，性质是否成立？ 状态空间可能爆炸，有限界限不等于无界证明
演绎式形式化验证 程序是否满足明确写出的逻辑规范？ 需要规范、证明义务和适当的工具支持

形式化验证不是一种更高级的单元测试。它试图回答的问题更强：在给定前置条件、程序语义和证明假设的前提下，程序是否满足指定的后置条件。

以求和函数为例，我们希望建立这样的数学关系：

Sum(n) = n * (n + 1) / 2

但这条公式还不够。我们需要进一步说明：

  • 输入 n 的合法范围是什么？
  • 循环过程中，部分和应该满足什么关系？
  • 函数返回时，如何从循环状态推导出最终结果？
  • 如果使用 Go 的有限位宽整数，整数溢出是否会影响结论？

最后一个问题尤其重要。数学中的整数通常没有固定的位宽，而 Go 的 int 是有限位宽的机器整数。若忽略溢出，数学上的证明未必能直接转化为对实际机器程序的完整保证。

形式化验证要求我们把这些假设说清楚，而不是默认它们不存在。

这也解释了为什么形式化验证通常需要比测试更多的前期思考。测试告诉我们程序在某些输入下做了什么；规范则必须明确地表达程序应该做什么。

Go 并不是形式化验证的荒漠：认识 Gobra 与 Viper

谈到形式化验证，很多程序员首先想到的是 Coq、Lean、Isabelle，或者专门为验证设计的语言。

但对于已经拥有大量 Go 代码的团队而言，一个更现实的问题是：能不能尽量保留现有的 Go 编程方式，在其上增加机器可检查的正确性约束？

答案是可以尝试。

这里最值得重点介绍的项目之一，是 ETH Zurich Programming Methodology Group 开发的 Gobra。

Gobra 是一个自动化、模块化的 Go 程序验证器，主要面向包含堆状态操作与并发行为的程序。它允许开发者为 Go 程序添加前置条件、后置条件、断言、循环不变量等规范，再由验证工具检查这些条件是否成立。

它并不要求开发者把整个业务系统改写成一种全新的证明语言。相反，它尽可能保留 Go 的程序结构，同时引入表达正确性所需的注解。

Gobra 背后的 Viper 是什么？

Viper 并不是一个专门针对 Go 的工具，而是一套用于构建程序验证器的基础设施。

它提供中间验证语言、规范表达机制和验证后端。不同语言的验证工具可以将源程序转换成 Viper 能理解的形式，再利用底层验证引擎检查程序是否满足规范。

ETH Zurich 团队在 Viper 之上构建了多个验证器，其中就包括面向 Go 代码的形式化验证器 Gobra。

这套架构可以简化为：

这里的几个组件各有职责。

第一层是 Gobra。它理解 Go 程序及其规范，并将验证失败的信息尽可能映射回开发者熟悉的源代码层面。

第二层是 Viper。它提供用于表达程序状态、断言和权限的统一验证模型。Gobra 不必从零实现所有底层的逻辑推理机制。

第三层是验证后端和 SMT 求解器。例如，Silicon 使用符号执行思路，并通过 Z3 求解逻辑约束。对于满足特定条件的验证义务，工具可以自动完成大量推理。

这种分层设计的价值在于，验证器不必完全绑定于某一种源语言。不同语言可以共享底层验证技术，而前端负责处理各自的语言语义。

Gobra 能验证什么？

根据项目文档，Gobra 支持 Go 的一个较大子集，包括接口和多种常见数据结构，并覆盖一系列重要的程序性质：

  • 功能正确性。例如，函数返回值是否符合数学规范。
  • 内存访问与权限约束。例如，访问指针所指向的数据前，是否拥有相应的访问权限。
  • 数据竞争相关性质。通过权限的转移和共享状态约束，检查并发访问是否符合模型。
  • 部分正确性。在程序终止并返回的前提下，是否满足指定的后置条件。
  • 终止性。在适当的注解与证明条件下，还可以对程序是否终止进行推理。

这里需要特别说明：Gobra 的能力并不意味着任意 Go 程序都能不加修改地完成验证。它只支持 Go 的一个子集，特定语言特性、第三方依赖和复杂的程序结构可能需要额外的规范、建模或人工处理。

它也不是简单地把 go test 的结果包装成一个“证明成功”的标记。

真正的关键在于，Gobra 允许开发者将程序的正确性要求写成机器可以处理的逻辑条件。

实战：让机器证明一个 Go 求和算法

抽象概念说得再多，不如看一段真正的代码。

我们继续使用求和函数。它足够简单，可以让我们集中注意力观察证明过程，而不是被业务细节淹没。

Gobra 官方教程提供了一个相似的例子：求出从 0 到 n 的整数之和，并使用前置条件、后置条件和循环不变量进行验证。下面沿用其核心结构。

先写出普通的 Go 程序

创建文件 sum.go：

package main

import "fmt"

func Sum(n int) (sum int) {
    sum = 0
    for i := 0; i <= n; i++ {
        sum += i
    }
    return sum
}

func main() {
    fmt.Println(Sum(5))
}

运行：

go run sum.go

输出：

15

这说明程序对输入 5 给出了预期结果。但它不能证明对所有合法输入，程序都会返回正确的结果。

我们当然可以继续补充测试：

func TestSum(t *testing.T) {
    tests := []struct {
        n    int
        want int
    }{
        {0, 0},
        {1, 1},
        {5, 15},
        {10, 55},
    }

    for _, tt := range tests {
        if got := Sum(tt.n); got != tt.want {
            t.Errorf("Sum(%d) = %d, want %d", tt.n, got, tt.want)
        }
    }
}

这些测试很有价值，但它们依然只检查了有限个输入。

现在，我们换一种思路：不再问“这些输入有没有算对”，而是明确要求机器检查整个函数是否满足一组数学性质。

给函数写上正确性契约

Gobra 在 Go 程序上增加了专用的规范注解。一个函数可以通过 requires 表达前置条件，通过 ensures 表达后置条件。

例如：

requires 0 <= n
ensures  sum == n * (n+1)/2

这两行分别表达了什么？

requires 0 <= n 表示调用者必须保证输入非负。

ensures sum == n * (n+1)/2 表示函数返回时，返回值必须符合求和公式。

将它们与循环不变量结合，就可以构成一个演绎式验证任务。

不过，直接把这两行贴到普通 Go 文件里，并不能让标准 Go 编译器自动完成形式化验证。Gobra 有自己的注解语法和验证工具链，需要使用对应的验证器处理程序。

用循环不变量连接程序与数学证明

完整的 Gobra 示例如下。保存为 sum.gobra：

package tutorial

requires 0 <= n
ensures  sum == n * (n+1)/2
func Sum(n int) (sum int) {
    sum = 0

    invariant 0 <= i && i <= n + 1
    invariant sum == i * (i-1)/2
    for i := 0; i <= n; i++ {
        sum += i
    }

    return sum
}

这段代码采用 Gobra 官方教程中的注解形式。它不是一份可以直接交给普通 Go 编译器编译的文件，而是交给 Gobra 验证器处理的源文件。

两个 invariant 注解，才是这个例子最值得关注的地方。

第一个不变量：

invariant 0 <= i && i <= n + 1

它规定循环变量始终位于合理范围内。循环开始前，i 从 0 开始；循环结束时，i 可以到达 n+1。

第二个不变量：

invariant sum == i * (i-1)/2

它描述了循环变量和部分求和结果之间的关系。

当 i 等于 0 时，sum 是 0，等式成立。

每轮循环执行 sum += i，然后循环变量递增。假设原来的部分和满足：

sum = i * (i - 1) / 2

那么更新之后：

sum'= sum + i

代入原有关系：

sum' = i * (i - 1) /2 + i

整理可得：

sum' = i * (i + 1) / 2

当循环结束时，i 等于 n+1。因此：

sum = ( n + 1) * n / 2

这恰好就是我们要求的后置条件。

整个证明的结构非常清晰：

这就是循环不变量的核心作用：它不是对代码执行过程的注释，而是将每一次循环迭代与最终的数学结论连接起来的证明工具。

怎样真正运行 Gobra？

Gobra 的安装比普通 Go 工具复杂。根据其官方仓库说明，需要准备 64 位 Java、SBT、Git，以及与当前工具版本兼容的 Z3。

注：若使用默认的 Silicon 后端，不需要额外配置 Boogie；使用 Carbon 后端时则需要相应依赖。

以下以官方仓库为入口：

git clone https://github.com/viperproject/gobra.git
cd gobra

git submodule update --init --recursive

sbt compile
sbt assembly

构建成功后，官方 README 给出的默认产物路径是：

target/scala-2.13/gobra.jar

设置 Z3 可执行文件的路径：

export Z3_EXE=/absolute/path/to/z3

然后使用 Gobra 验证器处理示例：

java -Xss128m -jar target/scala-2.13/gobra.jar \
  -i /absolute/path/to/sum.gobra

这里的 /absolute/path/to/z3 和 /absolute/path/to/sum.gobra 都需要替换为本机上的真实路径。

在我的 Mac 环境下，执行结果类似：

Gobra 0.1.0-SNAPSHOT (d2c5af5450540c502855e53f4a5af1ba7630c41f)
(c) Copyright ETH Zurich 2012 - 2026
16:01:06.694 [main] INFO viper.gobra.Gobra - Verifying package /Users/tonybai/go/src/github.com/viperproject/gobra - tutorial [16:01:06]
16:01:08.625 [thread-7] INFO viper.gobra.Gobra - Gobra found 0 errors.

如果我们故意把循环不变量改错（比如把 -1 改成了 +1）：

package tutorial

requires 0 <= n
ensures  sum == n * (n+1)/2
func Sum(n int) (sum int) {
    sum = 0

    invariant 0 <= i && i <= n + 1
    // 故意改错：原来是 i * (i-1)/2，改成 i * (i+1)/2
    invariant sum == i * (i+1)/2 
    for i := 0; i <= n; i++ {
        sum += i
    }

    return sum
}

再运行 Gobra，就会得到类似下面的错误：

Gobra 0.1.0-SNAPSHOT (d2c5af5450540c502855e53f4a5af1ba7630c41f)
(c) Copyright ETH Zurich 2012 - 2026
16:00:58.955 [main] INFO viper.gobra.Gobra - Verifying package /Users/tonybai/go/src/github.com/viperproject/gobra - tutorial [16:00:58]
16:01:01.077 [ForkJoinPool-3-worker-1] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <sum.gobra:10:15> Loop invariant might not be preserved. 
Assertion sum == i * (i+1)/2 might not hold.
16:01:01.086 [thread-4] ERROR viper.gobra.Gobra - Gobra found 1 error.

另一个重要细节是整数溢出。上面的数学推导将整数关系作为核心，但真实 Go 程序使用有限位宽的 int。对于可能接近机器整数上限的输入，不能只凭数学公式就认定实际实现正确。生产级规范需要明确输入范围和溢出处理策略，并确认这些条件在目标验证器的整数模型中得到了正确表达。

这恰好体现了形式化验证的价值：它迫使我们把平时容易忽略的假设，变成明确的验证义务。

真正的难点不是加法，而是指针、切片和并发

求和函数是入门例子。对于实际的 Go 服务，真正有价值、也更困难的验证任务，往往涉及可变状态、共享内存和并发访问。

Go 程序大量使用指针、切片、结构体、接口、goroutine、channel 和 mutex。这些机制让 Go 很适合编写高并发服务，但也让程序的正确性不再只是几个简单的数学等式。

例如：

type Counter struct {
    Value int
}

func Inc(c *Counter) {
    c.Value++
}

单看这段代码，很难说有什么问题。

但如果两个 goroutine 同时调用 Inc，而访问之间没有适当的同步，那么就可能发生数据竞争。

常规测试可能因为执行时序不同而没有发现问题。go test -race 可以帮助检测实际执行中出现的数据竞争，但它同样不是对所有可能执行时序的完整证明。

Gobra 的一个重要特点，是采用权限逻辑来推理可变状态。

权限逻辑：谁可以读，谁可以写？

在普通代码审查中，我们通常通过阅读代码来判断某个指针是否会被多个 goroutine 同时访问。

权限逻辑尝试将这类约束表达成机器可以检查的规范。

Gobra 使用 acc 等访问权限断言，描述当前函数是否拥有访问某个内存位置的权限。对可变状态的写入通常需要相应的独占写权限，而权限可以根据函数契约在调用者和被调用者之间转移。

下面是 Gobra 官方教程中的典型结构：

package tutorial

requires acc(x)
ensures acc(x)
func inc(x *int) {
    *x = *x + 1
}

这段注解表达的是：函数调用前，调用者必须拥有对 x 所指向位置的访问权限；函数返回后，权限应当归还。

当程序启动一个 goroutine 时，权限也需要按照相应的并发规范进行转移。如果第一个 goroutine 已经获得了独占访问权限，调用者就不能再把同一份独占权限交给另一个 goroutine。

因此，某些潜在的数据竞争会在验证阶段被拒绝，而不必等到程序在生产环境中恰好执行出问题。

这不是说 acc 本身就能自动消除所有并发错误。它的作用是把内存访问与所有权约束纳入证明体系，最终结果仍然取决于规范是否完整、程序是否满足这些规范，以及所使用的并发模型是否覆盖目标行为。

为什么切片和接口也需要规范？

Go 的切片并不只是一个普通数组。它涉及底层数组、长度、容量以及多个切片之间可能存在的别名关系。

假设一个函数需要把切片中所有元素加上一个数：

func AddToSlice(s []int, n int) {
    for i := range s {
        s[i] += n
    }
}

我们除了要证明每个元素的更新符合预期，还需要说明：

  • 所有访问的下标都在合法范围内。
  • 调用者提供了足够的内存访问权限。
  • 函数返回时，访问权限按照契约得到保留或归还。
  • 对于需要证明的功能性质，切片中的每个元素都满足相应的后置条件。

Gobra 的官方教程展示了如何用量化断言表达对切片元素的权限，以及如何描述更新前后的元素关系。对于链表等递归结构，它还可以使用谓词来抽象复杂的内存布局。

这些机制的价值在于，开发者可以把“这段代码应该如何访问内存”从隐含的编程约定，变成明确的形式化约束。

当然，越接近真实业务系统，证明工作通常就越复杂。复杂的接口分派、外部库、动态行为、共享状态和第三方依赖，都可能要求更多规范或额外的抽象。

形式化验证不是免费的。它用明确的建模与证明成本，换取更强的正确性证据。

AI Agent 能否把形式化验证的成本也降下来？

看到这里，一个自然的问题是：既然形式化验证需要开发者编写规范、设计不变量，甚至处理复杂的权限关系，那么它会不会只是少数形式化方法专家的专属工具？

这正是 AI Agent 可能改变的地方。

传统形式化验证的瓶颈之一，不一定是验证器本身，而是人类必须把程序意图翻译成机器能够理解的逻辑表达式。

开发者知道一个函数应该返回什么，却未必知道如何写出足够精确的后置条件；知道循环应该结束，却不一定能立即找到合适的不变量；知道两个 goroutine 不应该发生数据竞争，却未必熟悉权限逻辑的全部表达方式。

大模型恰好擅长根据代码上下文提出候选方案。

但必须区分：生成一个看起来正确的证明，与让一个可信的验证器接受这个证明，是两件不同的事。

让 Agent 负责提出候选规范

假设开发者给 Agent 一个任务：

“实现一个函数，对整数切片进行原地累加。要求所有元素增加指定的值，切片长度不变。”

Agent 可以先生成普通 Go 实现，再尝试生成对应的形式化规范。

例如，针对元素更新，它可能提出类似这样的后置条件：

这个表达式描述了每一个合法下标处，修改后的元素都等于原值加上 n。

接下来，Agent 还可以根据循环结构生成候选不变量，描述已经处理的部分和尚未处理的部分分别满足什么性质。

这些内容并不保证第一次就正确。Agent 可能遗漏别名问题，可能生成不够精确的规范，也可能给出无法证明的不变量。

但它至少可以承担大量候选生成工作。

让验证器负责作出判断

Agent 提交候选规范后，Gobra 负责检查程序是否满足这些规范。

验证失败时，工具可能指出某个断言无法证明，或者某个访问权限不满足要求。Agent 可以据此调整实现、修改不变量，再次提交验证。

这个过程与 AI 自动修复编译错误很像，但目标不同。

编译器检查的是程序是否满足语言的语法和类型规则；形式化验证器检查的是程序是否满足更高层次的逻辑性质。

一个程序即使可以成功编译，也可能在某个边界条件下违反后置条件。

整个协作过程可以表示为：

这个流程中最重要的设计原则是：模型可以建议，但不能替代验证器作出正确性结论。

如果 Agent 生成了错误的不变量，验证器应当拒绝它，而不是因为模型信心十足就放行。如果 Agent 修改了规范，使一个原本失败的证明变得容易通过，开发者还必须确认规范没有被悄悄削弱。

否则，系统可能陷入一种危险的循环：为了让验证通过，不断降低需要验证的要求。

为什么不能让第二个大模型来当裁判？

一个常见的想法是：让一个模型写代码，再让另一个模型审查。

这种方式有价值，能够发现不少问题。但它仍然属于基于模型判断的审查机制。

两个模型可能共享相似的训练数据、推理偏差和错误假设。第二个模型即使给出详细解释，也不等于提供了可机器检查的证明。

FATTW 2026 的报告强调了这一差异：形式化验证的价值不只是“再检查一次”，而是将正确性判断交给可以独立检查逻辑义务的验证机制。

当然，验证器也并非天然绝对可信。工具实现可能存在缺陷，源程序到中间语言的转换可能有问题，底层求解器与运行环境也存在各自的信任边界。因此，形式化验证提高的是特定假设下的正确性保证，而不是对整个软件供应链作出无条件承诺。

除了 Gobra，Go 还有哪些形式化验证路线？

Gobra 值得重点关注，但它不是 Go 形式化验证研究的全部。

VeGo：直接在标准 Go 源码中表达规范

2026 年 8 月公开的论文《VeGo: Direct Deductive Formal Verification of Go Programs for Computer Science Education》，提出了另一条路线。

VeGo 的目标是直接验证标准 Go 源码，并使用特殊注释表达契约、循环不变量、终止性度量和等式推理等内容。

它的设计重点之一，是尽可能让带注解的文件仍然保持标准 Go 源码的可编译性，使学习者不必完全离开日常使用的编程语言，就能接触演绎式验证。

不过，这篇论文的定位偏向计算机科学教育，不能直接把它视为已经成熟、可全面替代生产级工具的 Go 验证方案。它提出了值得关注的技术路线，但工具的适用范围、工程成熟度与实际生产验证能力，仍需要结合项目发展和独立评估来判断。

其他值得关注的方向

除 Gobra 和 VeGo 外，还可以从几个方向观察 Go 的形式化验证生态：

  • 基于 SMT 求解器的演绎验证。将程序性质转化为逻辑约束，借助自动定理证明与约束求解技术检查正确性。
  • 符号执行与模型检查。探索可能的执行路径，查找违反断言的输入或状态。它们在检测运行时错误和分析并发行为时尤其有用，但有界探索不应被误认为无界正确性证明。
  • 程序逻辑与分离逻辑。通过所有权、访问权限和状态不变量，推理复杂数据结构与并发程序的行为。

这些路线之间存在交叉。Viper 本身就是一个很好的例子：它提供共享的验证基础设施，让不同前端和验证技术可以复用底层能力。

对于实际工程团队，选型时不能只比较工具是否宣称支持“形式化验证”，还要看它支持多少 Go 语言特性、如何处理第三方依赖、是否能集成到 CI，以及规范维护成本是否符合团队的工程预算。

Rust 的 Verus：同一趋势下的另一条路线

Rust 也有值得关注的工具，例如 Verus。

Verus 允许开发者在 Rust 程序中表达规格与证明相关信息，并针对程序性质进行演绎式验证。它的设计与 Rust 的类型系统、所有权和借用机制相结合，目标是帮助开发者证明比内存安全更强的程序性质。

需要注意，Rust 的所有权系统已经能够在语言层面排除许多内存安全问题，但它并不能自动保证所有业务逻辑都正确。一个没有数据竞争、没有非法内存访问的程序，仍然可能计算出错误的金额、执行错误的状态转换，或者违反协议约束。

这与 Go 面临的问题并无本质区别：语言层面的安全保证很重要，但功能正确性仍然需要单独表达和验证。

真正的挑战：不是证明一个函数，而是证明一个系统

看到 Gobra 的例子，很容易产生一种乐观的想象：既然简单函数可以证明，那么是不是可以让 AI 为整个 Go 项目自动生成规范，再把所有代码都验证一遍？

从技术方向上说，这是值得探索的目标。但从当前工具的能力和工程实践看，距离这个目标仍有很大差距。

一个真实的 Go 服务可能包含 HTTP Handler、数据库事务、缓存、消息队列、重试机制、分布式锁，以及大量第三方依赖。函数本身的正确性只是系统正确性的一部分。

假设我们要验证一个转账服务：

func Transfer(from, to *Account, amount int64) error

我们真正关心的，可能不仅是函数有没有 panic，还包括：

  • 转账成功时，付款账户余额减少的金额是否等于收款账户增加的金额。
  • 任意失败路径上，系统是否可能只扣款而没有入账。
  • 两个并发转账操作是否可能导致余额不一致。
  • 重试是否可能重复执行已经成功的操作。
  • 数据库提交成功但响应丢失时，客户端重试是否会造成重复扣款。

其中有些性质可以通过函数契约和状态不变量表达，有些涉及数据库事务、分布式系统行为与外部组件语义，需要进一步建模。仅仅验证一个 Go 函数，不能自动推出整个分布式系统满足所有业务要求。

这也说明，形式化验证的真正工程价值，不在于给每一行代码都贴上一个“已证明”的标签，而在于找到那些最值得投入验证成本的关键性质。

对于 Go 项目，可以从以下几个方向逐步推进。

第一，先选择边界清晰的核心算法。例如金额计算、配额分配、状态转换、协议解析，以及容易出现边界条件错误的算法。这类代码通常有较明确的输入输出关系，更适合首先引入前置条件和后置条件。

第二，把关键业务不变量写清楚。例如余额不能为负、状态转换必须遵循合法顺序、某些资源不能被重复释放。即使暂时无法完成完整的形式化证明，明确规范本身也能提高代码审查与测试的质量。

第三，逐步验证共享状态和并发边界。对于使用 mutex、channel 和共享数据结构的代码，可以探索 Gobra 的权限模型，验证特定的内存访问与并发约束。

第四，将验证纳入持续集成。当验证成本和工具适用范围允许时，可以将形式化验证作为关键模块的 CI 检查。与测试、静态分析和代码审查结合，形成多层质量保障机制。

第五，让 AI Agent 参与规范与证明的维护。Agent 可以帮助生成候选规范、补充不变量、分析失败信息并尝试修复。但规范变更必须经过审查，验证器的实际结果也必须被保留，不能只记录模型给出的结论。

形式化验证并不是要取代测试。测试依然擅长验证集成行为、环境交互和真实运行效果；静态分析依然可以低成本发现大量常见问题；代码审查则负责理解业务意图、架构边界和维护成本。

这些技术应该互相补充，而不是互相取代。

小结：未来的代码审查，可能不再只是阅读代码

回到文章开头的问题。

AI 时代，写出一段能够编译、能够运行的代码，正在变得越来越容易。但软件真正需要的，不只是能够运行的实现，而是满足需求、经得起边界条件考验、能够在长期演进中保持正确的实现。

数学领域的 Lean 展示了一个重要方向：AI 可以提出证明，机器可以独立检查证明是否成立。

Go 领域的 Gobra 与 Viper，则尝试把类似的思想引入实际程序。通过明确的前置条件、后置条件、循环不变量和权限模型，我们可以让一部分原本依赖人工判断的程序性质，转化为可机器检查的验证义务。

这条路还没有走到终点。工具支持范围、规范编写成本、第三方依赖、复杂并发语义以及验证基础设施自身的可信度，都需要持续改进。但它已经提供了一种不同于“让 AI 再检查一遍代码”的思路。

未来的软件工程工作流，可能逐渐形成这样的分工：

  • AI Agent 负责快速生成实现、提出规范和探索证明。
  • 编译器、测试与静态分析工具负责检查各自覆盖范围内的问题。
  • 形式化验证器负责检查能够严格表达的正确性性质。
  • 人类开发者负责确认需求、审查规范、设计架构，并承担最终的工程责任。

AI 让代码越来越便宜，可信的正确性证据却不会自动变得便宜。

真正值得期待的，不是某一天所有程序都不再需要人类审查，而是我们能够把越来越多关键的正确性要求变成明确的规范，让机器承担可以自动化的证明工作。

对于 Go 开发者而言，Gobra 是一个值得亲自研究和试验的起点。对于整个 AI 软件工程领域而言，如何让大模型生成的代码不仅能够运行，而且能够被独立验证，或许才是下一阶段真正值得投入的方向。

参考资料：

  1. Lucas C. Cordeiro，Formal Verification of LLM-Generated Code，FATTW 2026。- https://ssvlab.github.io/lucasccordeiro/talks/fattw2026_slides.pdf
  2. ETH Zurich，Viper: Verification Infrastructure for Permission-based Reasoning - https://www.pm.inf.ethz.ch/research/viper.html
  3. Viper Project，Gobra: An Automated, Modular Verifier for Go Programs。- https://github.com/viperproject/gobra
  4. Viper Project，A Tutorial on Gobra。- https://github.com/viperproject/gobra/blob/master/docs/tutorial.md
  5. Tina Massoudi、Chris Dutchyn，VeGo: Direct Deductive Formal Verification of Go Programs for Computer Science Education，2026。 - https://arxiv.org/abs/2608.22630
  6. OpenAI，Sharing AI Progress in Mathematics，2026。- https://openai.com/index/sharing-ai-progress-in-mathematics
  7. Verus 项目 - https://github.com/verus-lang/verus
  8. Geoffrey Huntley，原始讨论。- https://x.com/GeoffreyHuntley/status/2111404174147752026

还在为写 Agent 框架频频死循环、上下文爆炸而束手无策？我的新专栏 《从0 开始构建 Agent Harness》 将带你：

  • 抛弃臃肿框架，回归“驾驭工程 (Harness Engineering)”的第一性原理
  • 用 Go 语言手写 ReAct 循环、并发拦截与上下文压缩引擎等，复刻极简OpenClaw
  • 构建坚不可摧的 Safety Middleware 与飞书人工审批防线
  • 在底层实现 Token 成本审计、链路追踪与自动化跑分评估
  • 从“调包侠”进化为掌控大模型边界的“AI 操作系统架构师”

扫描下方二维码，开启从 0 开始构建Agent Harness 的实战之旅。

还在为“复制粘贴喂AI”而烦恼？我的新专栏 《AI原生开发工作流实战》 将带你：

  • 告别低效，重塑开发范式
  • 驾驭AI Agent(Claude Code)，实现工作流自动化
  • 从“AI使用者”进化为规范驱动开发的“工作流指挥家”

扫描下方二维码，开启你的AI原生开发之旅。

商务合作方式：撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。如有需求，请扫描下方公众号二维码，与我私信联系。