一、项目背景

Sybase数据库在国内电信、政务、交通有大量存量系统，业务端用Sybase官方的CT-Library开发：

ct_con_alloc(ctx, &con);
ct_command(cmd, CS_LANG_CMD, sql, CS_NULLTERM, CS_UNUSED);
while (ct_results(cmd, &restype) == CS_SUCCEED) { ... }

这些调用散布在几百个源文件里。信创迁移到达梦数据库时，两条路：

• 改应用：把上面每一处 ct_* 换成达梦的 DPI 接口。改动量以人月计，且改完还要重新测一遍业务。
• 做兼容层：在达梦的 DPI 之上，重新实现一套兼容Sybase的API。应用不改代码，链接时换一个 .so / .dll 就行。

我们走的是第二条路：

应用 → ct_* → 兼容驱动 → dpi → 达梦

兼容驱动的接口需要一个一个对着官方手册实现。
这是典型的"接口规约明确、实现细节琐碎"的活，非常适合交给 AI 生成，也正是因此埋下了后面的坑。

二、痛点：AI 写得出代码，但没人敢用

2.1 产能过剩，验证欠债

AI生成的代码产能惊人：几万行C代码，跨CS/CT/BLK三套API，涉及数据类型编码、LOB流式传输、BLK批量协议。
按传统节奏要以月计，AI能在很短时间内成型。

但交付物的状态是尴尬的："能跑通 Hello World"和"可以上生产"之间隔着一整个可靠性工程。

2.2 数据库的缺陷特别隐蔽

对于数据库兼容驱动，很多bug形态是：

• 不崩溃、不报错、返回成功，然后数据入库错误
• 第一次能跑，第二次报一个没人认识的 -70027

这类bug很难在冒烟测试里露头，但可能在客户的生产库里露头。

2.3 人工测试验证这条路走不通

对一个163个函数的库，人工验证的问题是：

• 写得过来吗：不同的执行路径组合（每个函数3~10条路径），庞大的类型映射矩阵（几十种「源数据类型 × 目标数据类型」组合），调用序状态机（ct_send / ct_results / ct_fetch的不同调用顺序）——用例数是千级的。
• 想得到吗：某个堆越界写的bug，需要同时满足五个条件才会触发，任何一条没想到，测例就写不出来。
• 测得完吗：跑一遍测例、定位、改、回归——每轮以天计。而 AI 生成代码的速度是分钟级，验证速度比生成速度慢两个数量级。

一句话总结痛点：AI 把写代码的成本打下来了，于是验证成了新的瓶颈；而验证恰恰是最依赖人、最难规模化的环节。

三、解法：通过AI与形式化结合 先把「应该做什么」写成规约，再拿规约查代码

我们调研了一些自动化代码验证工具，最终选择了FM-Agent —— 上海交大王肇国教授团队推出的形式化方法智能体。

3.1 核心思想

不写测试用例，而是写规约——每个函数"前置条件是什么、执行后保证什么"。这就是霍尔逻辑的三元组 {P} C {Q}，只不过用自然语言+大模型推理。

规约描述调用方期望的正确行为，而AI生成的代码实现可能与规约不匹配，这就是bug。

3.2 规约长什么样

规约只写"要什么"，不写"怎么做"

函数：`dm_stamp_to_time` —— 把时间戳转成time类型
前置条件：`stamp` 是一个填好的时间戳；`out` 是一块能放下一个 `CS_TIME` 的内存。
后置条件：
  - 结果：成功时 `out` 里是时、分、秒、亚秒换算出的计数，全程整数运算，不足一个 tick 的余数丢掉、不进位；
  - 返回码：只有时分秒都在范围内（0–23 / 0–59 / 0–59）才返回成功，否则返回失败，且 `out` 里的内容不可信；
  - 一致性：相同的输入必须得到相同的输出；
  - 副作用：不分配内存、不保留指针、不产生诊断。

这几条看着朴素，但每一条都能被一个具体输入证伪，实现机器自动验证。

比如"不进位"这一条，只要构造一个亚秒不能被一个tick整除的输入跑一遍——进位了就是bug，没进位就是对的，没有中间状态。规约如果写成"正确处理时间戳"，机器就没法判断什么算正确，也就没法自动验证，只能靠人去看。

3.3 FM-Agent 的流程

FM-Agent 把整个过程做成三步：

1. 规约生成——自己根据文档和代码读懂系统设计意图，为每个函数写出正确性规约；
2. 代码推理——不用人工干预，自动推理代码实现是否满足规约；
3. 缺陷诊断——对有问题的函数，分析出bug的位置和根因。

四、结果

指标	数值
模型	deepseek-flash
覆盖	21 文件 / 163 函数 / 10 模块
耗时	2 小时
成本	10.39 美元
结果	发现 181 个疑点 → 报告缺陷 98 个 → 已人工确认真实缺陷 31 个

10 美元、2 小时、163 个函数的规约与 98 个疑似bug。 这是人力不可能达到的性价比——按传统方式，光把 163 个函数的单元测试覆盖率写到90%，就是一两个人月。

31 个真实bug覆盖的类别，说明了FM-Agent能弥补哪些人工容易漏的地方：

类别	代表	人工测试的覆盖难点
内存安全	32位乘法溢出导致堆越界写	需同时凑齐多个非常规前置条件
数据正确性	陈旧字典缓存；静默截断	不崩溃不报错，测试全绿，上生产才崩溃
可观测性	数据入库错误但返回码是成功	测例只查返回码，不查数据是否正确
资源与生命周期	ct_init 半初始化 + 句柄泄漏	失败路径很少有人构造

五、意义

AI时代，数据库研发的痛点从来不是"写不出代码"，而是"写完不敢用"。

我们这一次给出的答案是：根据官方文档定义兼容接口 + AI 生成代码 + FM-Agent 自动验证，可以以10 美元 / 2 小时的成本，把 163 个函数的正确性过一遍。

我们没有让 AI 变成"可以盲信"，而是让 AI 生成代码从"未知风险"变成了"已知缺陷列表"——这在工程上是从 0 到 1 的差别。

FM-Agent 给出的不是"建议检查一下这里"，而是详细缺陷报告 + 可执行的复现测例——这正是一个自动验证工具该有的样子。它延续了霍尔逻辑的核心思想，借助大模型的强大推理能力，实现了全自动正确性推理，为 AI 时代的软件验证提供了新的可行路径。