英文文化适配版： A Generalized Curry–Howard Proof Searcher and Program Synthesizer (English cultural adaptation)

书接上回： 明系魔法吟唱之5 – 我要说的事，你们千万别害怕

距离上一篇文章已经过去五个多月，这段时间里 AI 的玩法也发生了翻天覆地的变化。回想上半年，多少神棍（AI 导师）扬言软件开发已经被 AI 彻底解决， 99% 程序员都可以裁掉，甚至扬言软件开发已经进入黑灯工厂时代。各大技术分享会议的议题也只剩下了 AI 一个主题，大厂高 P 架构师们满世界宣传 AI 是如何给自己研发部门提效的，交付量增加了多少，工期一再缩短。甚至不乏有水货架构师自信地将提交次数和代码行数的巨幅增长当作提效的证据，在演讲中展示，似乎觉得代码行越多越好。但进入到下半年后，却又有冷却的迹象，甚至我在的最神棍的群也少有人讲这些神话了。

昂贵的 token 烧了，代码量膨胀了数倍，开发每人每天都有几十次提交，最终交付的功能却没变多，质量下滑得还越来越快。裁员、解散团队省下来的钱，甚至远超 API token 账单。¹

而基座模型的智力则每周突飞猛进，连评测题目的难度都越来越不够用，模型公司甚至开始挑战起了千禧年猜想。要是题目和 bench 方法不更新，怕是熬不到年底考卷就要被刷成满分了。²

一边是 Coding Agent 们刷分再创新高，AGI 时代又双叒叕一次到来，无缝衔接的核爆将我瘫在椅子上动弹不得。C 家刚把黎曼猜想比例已知下界提升到 67.2%. O家又攻克了 N-S 方程。一边是 AI 长期维护的工程越来越屎，代码行数越来越多，问题回归频率也越来越高。AI 在百年未结的千禧年猜想上屡建奇功的智力，似乎对长期维护的应用层软件帮助并不大。怎么？键盘撒把米，鸡都会写的 CRUD 业务系统，比黎曼猜想还难？

我在此留下暴论，AI 的科研能力确实得到了大幅进步，但复杂系统构建能力却并未能大幅提升。

1. 现在只有“民科”看出来了³

过去，形式化方法被束之高阁，只在关键系统内核、航空航天等领域使用。

我没学过 Lean，一行都没写过，甚至截至目前，入门书籍/教程/文档都没看过一行。而我的草台班子开发团队，算上我一共四个后端开发，其他三位同僚在 3 个月前甚至没有听说过 Lean。截至本文发布的今天，这套 Lean 4 后端已经在生产中滚动迭代了大约 3 个月。生产服务在这段时间没有停机。这说明：形式化方法不再只能待在编译器、内核和航空航天里，它可以进入需求朝令夕改的应用软件。

形式化方法已经被技术平权，可以在 AI 的辅助下“飞入寻常码农家”。

从年初的第一篇文章起，就设想了这个美好愿景，使用形式化验证来验收 AI 产出的逻辑代码。那时 AI 编写形式化代码并通过证明还很吃力，我也曾天真地低估 AI 发展速度，认为 AI 还要更长的发展时间才能在这个领域展露身手。 后来在第四篇里，我将“用前置条件、后置条件和不变量约束函数行为”的方法称为 Level 3。但能稳定落地的还是 Level 2 的类型、显式领域错误和副作用边界。 第五篇又往前走了一步：人类审查规范，AI 负责实现；抽取干净的核心覆盖形式化证明，脏的部分继续交给集成测试和 PBT。

最近几个月，我把过去设想的几个形式化与 AI 的结合方案全都在生产业务系统里实践了一遍，路线变迁了 4 次，证明形态也与我第四篇文章中 Level 3 的设想有很大区别。说实话，提出设想的时候觉得挺简单的，想当然地认为：

1. AI 会写形式化代码。
2. 形式化代码是图灵完备的。
3. 图灵完备的语言都能用来开发应用软件。

综上得出幼稚结论：AI 能用形式化语言开发应用软件。

就像 SMT 一样，每个函数都把要实现的需求写成 pre/post-condition。

最终实现效果嘛，它与我幻想中的形态有挺大差别，却又阴差阳错地带来了意外的收益。

2. 没有人记得它应该是什么样子

虚构故事：

FDE 部

ld： 小明小明！赵总的客户登不上平台了！你快看看怎么回事！

小明： 。。。我查一下。。。

ld： 先恢复！原因以后再查！赵总和老板还在客户现场，绝对不能再出故障了！

小明： 这几个账号没做实名认证，免费赠送额度也过期了，所以昨晚被自动清理了

ld： 啊？为什么！他们不是老赵的企业客户吗？

小明： 上个月产品上了实名认证功能
因为平台上真人注册的账号只有不到 3 千个，其他 40 多万账号都是机器人为了薅注册礼包创建的。
上周早会老板要求，所有账户必须强制实名认证，不通过的账号强制关闭。
还要求…

ld： 哎呀！你们开发做之前不动脑子的吗？老板指的肯定是个人用户，怎么能把企业用户也删了呢？快恢复

小明： 。。。

小明负责维护公司的 SaaS 产品。在 AI 编程的狂热席卷公司之前，这个项目还不到 2 万行代码。
短短几个月后，代码已经膨胀到了 90 万行。不可名状的架构，不可直视的细节。
代码越来越多，维护的人却越来越少。前端和测试团队都被裁撤了，仅剩的研发被笼罩在 AI“能工治人”的阴影下，渐失理智。

第二天事故复盘（批斗）会议

赵总先起头了：（阴阳怪气，故意用轻松戏谑的语气讽刺研发部门）
昨天我和 boss 在客户现场演示定制的功能，好不容易约到客户集团副总的时间。
本想在会上把下一季度的合同也签下来，我还在会上打包票，咱们研发技术很强，平台很稳定。
结果演示的时候他们 2 个同事账号都登录不上，吓得我一身冷汗。
多亏了老板力挽狂澜，当即让我切超管账号继续演示，这才……

ld： （上一个会议结束后，身体一直在不规律的震颤）

boss： （看向研发同事，语气很慢的说）今天不是批斗会，不追究谁的责任。事情已经发生了，关键是以后怎么避免。
我把这一周的群聊给 AI 看了一下。免费的，都能找出这些问题。（瞟了一眼 ld）研发要反思一下，为什么没提前看出来？

小明： （那你还嫌我们 token 用得多？事后诸葛亮谁不会，事前你的 AI 怎么不指出问题呢？）

ld： 小明，账户清理的模块是你上周开发的，这个 bug 你解释一下吧。

小明： 这个不是 bug，需求就是这么提的。会议纪要和变更文档也在飞叔群里发过，ld 你和产品都点了审批通过。

ld： 审批是通过了，技术风险你有没有提前提？
不能出了事才说需求就是这么写的。
我希望你有自己的判断。
如果研发不思考，那么很快就会变成下一个被 AI 取代的岗位。

小明： （终于找到发泄口了）

小明： 需求来得急，时间太紧了，根本没时间做详尽调研。

boss： 感受赋能，拥抱 AI，我今年一直在强调，研发部就没当回事儿。我们不是采购了企业知识库吗？会议纪要和需求都是 AI 自动整理到知识库里的。小明没时间的话，你让 AI 去调研不就行了？学一学产品部，AI 赋能后 3 个人做了过去 11 个人的工作，研发部要跟上时代。

小明： （AI 赋能？屎需求的生产速度我狠狠的感受到了，产品一天扔给我不下 10 份自相矛盾的万字需求文档。希望 AI 大人也能雨露均沾的让全公司感受一下赋能后屎山代码的崩溃力度。）

boss： 前几天我在群里分享的那几篇文章，OPC 公司 AI 工作流，大家要认真学习。人家一个人带几个 AI，产品、研发、运维这些角色全都有，AI 之间自己协调，三天交付一套系统。文章我都发群里了，研发部有没有认真看？现在的 AI 进化速度太快了，研发要积极配合 AI，不要拖 AI 的后腿。

小明： （三省六部制复辟了？老板这么热衷于 AI 角色扮演，公司干脆转型剧本杀吧。而且把我工牌印刷成 FDE 并不能加快交付速度，也不能提高交付质量。）

boss： 现在 token 都免费了，巴掌大的一个小盒子，什么模型都能跑。公司每个月还给研发报销 500 块的 AI 订阅……
你们研发这么大的电脑，起码能跑俩模型了。

小明： （喂喂喂！你要不要听听你自己在说什么，dgx spark 一台 3 万起步，公司配的黑砖头笔记本，体积大性能就高？）

…不知道讨论离题了多久…

ld： 继续说正事吧，小明你继续，复盘一下详细过程

小明： 按照上周二早会上老板提的紧急要求，个人账户必须通过实名验证才能继续使用。所以周三就部署了这个模块：每天 0 点清理一次未实名的非订阅账户

ld： 既然只针对个人，那为什么会清理掉企业账户呢？

小明： 被清理的不是企业账户，而是企业账户里的子账户。
spec 里记录了“所有实体账户都是个人账户”这个概念，是 ld 你定义的。

ld： 那这个账户也是关联到企业了呀

ld： 还有你说他们套餐到期了是什么意思？企业成员怎么会有套餐

小明： 我翻了二月份的 spec。当时定的是，新账户送一个月专业版，到期转免费。

小明： “企业版”是你们平时的叫法。系统里分团队版、企业版和外企版。
外企版先不说，系统里真正的企业版从来没有被用过。
这次受影响的是赵总的客户，因为历史原因，客户三个部门在系统里开了三个团队版。只有人事部门被波及，因为他们的成员都是通过外协邀请加入的，用的全是 QQ 数字邮箱。

ld： 可他们是邀请进来的啊，怎么又算注册用户了？

小明： 后台走的还是注册接口。spec 里有记录，接受邀请以后还要填名字和部门，这个 MR 就是 ld 你提交的。

ld： （…）既然这些信息都在 spec 里，那你为什么没有早预警这些风险？

小明： （既然你今天知道开盘涨停，昨天怎么不梭哈入场？）
为了这次复盘，10 个子代理跑了两个小时，才暴露出了这些问题，可能还有更多问题没被发现。
发生故障以后复盘很容易，发生故障以前 AI 也很难发现这些需求变更是互相冲突的。

boss： 技术细节你们会后单独讨论，复盘结束前要制定出流程，确保未来不会发生同样的问题。

小明： （复盘复盘，你们领导层怎么不复盘一下呢？）

ld： 这样吧，以后研发做需求变更时，用两个 agent 分别设计，并互相进行交叉验证，然后选最好的方案。
每次部署上线前，让 AI 评估影响范围列表，AI 点测一遍所有功能，最后研发和产品一起验收…
各位同事还有什么补充吗？小明你也提一下你的意见。

小明： （慢工出烂活，欲速则一坨。你把从设计到验收全都交给 AI，说明你也没当回事儿）

小明： 这样的话 AI 会更慢的，如果按照这个流程下来，三天都上不了线。我们工期压的太紧，应该先延长工期，这样才有时间做更充分的调研。

ld： 工期…（看了一眼老板，颤颤巍巍的说）…这个

boss： 你决定就行

ld： 好，那…那就低优先任务多加一…半天，半天吧，多给 AI 测试时间。紧急任务不变，这…样可以…吧（看向老板）

boss： 我只看最终结果

小明： (演！继续演！需求只有重要和很重要，交付只有紧急和很紧急。心里没数？)

小明： 不是没测。AI 连“确保这些外协账号被清理”的测试都写好了。
至于具体影响了哪些客户、有多少这种外协账户，不查生产数据库的话 AI 也不知道。

boss： （鬼点子生成中…生成完毕）那这样，后端直接不要写数据库了，直接写进知识库里，变更的时候让 AI 过一遍知识库，综合决策。

小明： （好家伙，不愧是古希腊掌管鬼点子的神）

ld： 老板这招妙啊，别的团队还在打破信息壁垒，我们直接一步到位，知识库作为单一信源（SSOT）…

小明： （还有高手，古希腊掌管马屁的神）

系统过去的假设散落在文档和知识库里，新设计又不断推翻旧设计。AI 想从这些文字里还原系统当前的行为，已经很难，还可能漏看或曲解。更何况文档是文档，实现是实现，并没有天地法则约束它们必须是一致的，同步是暂时的，偏离是永恒的。

3. 为上下文减负

“软件核心假设”并不是没有被留下记录。而是没有被持续的整理，检查，总结成为当下版本。哪些规则依然有效，哪些规则已经废弃。

当然，我相信这些信息散落在群聊记录，会议纪要，PRD，git log，代码注释，测试用例，以及代码当前实现中，但同时伴随着过时的信息，无关讨论，不准确的措辞，扭曲的架构，等技术债务。难道每次都让 AI 把相关上下文读一遍，独立推理出来吗？ 哪些规则还要保留，哪些已经废弃，哪些需要重新确认？废弃的规则又关联着哪些代码？这些都得重新理清，该删的旧规则和遗留代码也得清掉。可很少有人或 AI 敢做这件事。

形式化之前，我的项目 99% 代码由 AI 生成。每次出故障、翻代码的时候，我都能找到一些糟糕的遗留设计，它们产生于不同的 session，有些为了增加 feature，有的为了修复 bug。这些糟糕的设计已经变成前后冲突的流程逻辑，只等待机缘巧合时，某个运气不好的数据对象集齐了冲突条件，引爆这个地雷。

难道测试用例不能拦截这些冲突吗？难。大部分无法被测试用例发现，测试用例通常只能覆盖编写时部分分支走向，无法覆盖未来编写的分支。如果维护过程中修改了被调用基础函数（例如aop/日志/夹具函数），AI 会递归检查多少函数受到影响，并为这些函数补齐测试分支吗？

前后行为逻辑不一致，新功能加入破坏了过去的假设，甚至是关键假设，而 AI 没有意识到，人也不记得。我的软件第一版开发时，需求确实不多。但我会在后续迭代中补齐更多需求条件，或调整需求方向。而 AI 在实现我的需求的过程中，必然会加码（framework，middleware，db，component），且加的不少。迭代久了以后，哪些是我的真实需求，哪些是 AI 自己加码，已经无法分清了。而这些实现是否都服务于我现在（改了八百遍）的需求，更是无从得知。

我的 AI 为什么越跑越慢

• 为什么 AI 尝试在十几万行 C 模块中修复 bug？而这只是一个静态资讯网站项目 -> 因为这个 C 模块实现了向量检索能力，为 sqlite 提供语义搜索扩展
• 为什么要给 sqlite 增加语义检索支持？-> 因为项目使用了 sqlite 作为数据库
• 为什么技术选型定了 sqlite？ -> 因为这个项目最早是本地的个人笔记

接手的 AI 一看，项目已经投了这么多成本，便自然而然地选择继续在拧巴的路上拧巴下去。局部最优，屎山更高。

这当然不是一个真实的例子，但这个例子好就好在程序员读者能看懂。在 AI 超出你技术能力的领域，你敢保证你的 AI 没走类似的弯路？AI 给你写的天书般的代码，真的还服务于你现在的需求吗？

而用形式化定理描述软件的核心假设时，定理是可以被机器严格检查的，天然与当前代码行为一致。这远不是自然语言文字可以企及的。

我的做法是，从这些要求中选出一部分值得长期保护的性质，将它们写成形式化命题，并让相关实现承担证明义务。后续修改不能只满足这次新增的需求，还必须继续满足这些已经保留的约束。

最终，AI 不从自然语言文字中，也不从屎山代码里推理什么是当前正确的行为。

形式化不能替小明争取工期，也不能替老板决定哪些用户必须实名认证。它能帮助保留下来的，是那些已经确认、后续修改仍然需要满足的业务规则。

比如，个人套餐到期，不代表组织授予的使用权益也失效。后来增加“清理未实名的非订阅账户”这个需求时，AI 就更容易发现并提醒人类确认：这里的“非订阅”，指的是没有个人套餐，还是没有任何组织关系？

如果我们把组织授权对应的权益规则写进规格，并要求新的判定和清理逻辑继续满足它，AI 就不能只按这次需求写完代码、补完测试便交差。新旧规则若有冲突，要么修正对新需求的理解或实现，要么明确修改旧规则。形式化不替人做这个业务决定，但可以让已经写进规格的规则成为修改时必须面对的约束，而不是等事故发生，再从 spec 里考古。

这样一来，更多错误可以被拦截在开发阶段，老板岁月静好，开发负重前行。

4. 我最后造出来的东西

我现在是尽可能把业务状态、拒绝条件和 action 决策留在 Lean 里，做成纯计算，限死输入输出合约。repository 有一份带 invariant 的内存模型，一张表就是 Table = List DomainRow。

Service 从任意一个满足 invariant 的 repo 状态出发，产出新的合法 repo 状态和 action；也可以保持 repo 状态不变，只产出 action。相应的 Proofs 要证明这些状态转换仍然保持 invariant。初始状态合法，每一步又都保持合法，就像数学归纳法一样，可以一步一步往下走。

Repo 负责实际数据库的读写，Bridge 调用同一份决策，再把 action 交给执行器。

真实数据库这一侧，用 SQL + 约束实现和内存模型相同的 repository interface。内存模型里的 invariant 与数据库里的 table constraint 相互对应，两边的结构保持同构。SQL 和内存模型都摊开了，逻辑透明，审计难度也低，连低参数量的 AI 也能对照它们的行为是否一致。

PG 检查就是偏离检查：让内存模型和真实 PostgreSQL 中的 SQL 实现执行同一组操作，对照结果和状态。这是防止内存模型与 SQL 模型跑偏的一道自动化保险。

SQL、事务、锁、RLS、DDL、CAS 还是 PostgreSQL 实现；Firebase、对象存储、媒体、GPU 这些，交给 Rust/native sidecar。另有 wire 模块，检查 Lean 和 sidecar 之间的互操作 schema 是否对齐。数据迁移和整体验收，则分别由 migration、acceptance 检查负责。

1
2
3
4
5
6
7
8
9

人定义目标、状态迁移和不可牺牲的能力
             ↓
Agent 搜索程序、proof、引理和模块拆分
             ↓
Lean kernel 检查模型内的候选
             ↓
偏离检查 / wire 对齐 / migration / acceptance
             ↓
失败结果进入下一轮搜索

把自然语言翻译成严格的命题以后，原来的解释还是可以留在注释里，或者 link 到 PRD。 我关注的是定理。AI 以什么形式合成代码，只要能通过这些检查，我就不再逐行细看。 AI 滥用 axiom 和 sorry 欺骗验证可以直接被 #print axioms 捕捉到，这反而是最不容易作弊的。而 AI 翻译的一个或多个定理是否忠实反映原始需求，是否完全覆盖了需求，无法覆盖的裂隙是什么？

不需要在编码开始前把 spec 全部定死。我实际做下来发现，有些想当然的要求根本实现不了，只能一边实现一边补。 设计阶段觉得退款和到账是一步完成，写着写着才发现至少要经过支付网关，而且提交退款申请，银行卡到账都不是 100% 成功。

1
2
3
4
5

inductive Status where | approved | processing | refunded
structure State where
  balance : Nat
  order : Status
abbrev Step := State → Except State State -- 失败和成功都返回处理后的完整状态

这时候就把中间状态和失败路径补出来，拆成两条命题分别约束。也就是：在“一切正常”的前提下，退款最终会到账。

1
2
3

structure WeakSpec (amount : Nat) (submit settle : Step) : Prop where
  submit_post : ∀ s, submit s = .ok {s with order := .processing} ∨ submit s = .error s
  settle_post : ∀ s, settle s = .ok ⟨s.balance + amount, .refunded⟩ ∨ settle s = .error s

最后，一共就 3 条原则：

1. 对外部可信组件建模（例如 SQL 数据库，向量库，对象存储，SMS，支付网关等）
2. 对内部开发的组件约束输入输出合约
3. 将业务需求翻译成定理

最终，由经过严格验证的 Lean 代码来驱动和调度所有组件。

5. 无孔不入的腐化

刚才退款到账的例子中，失败路径写得挺像那么回事：如果退款申请失败，用户余额不会增加，订单状态不会改变。 那我所有请求都返回退款失败，不就完了？数据库一行不动，失败后置条件全都满足。唯一的问题是，谁也无法退款。因为规格没说，什么条件下才能判定退款成功。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

def alwaysFail : Step := fun s => .error s
theorem alwaysFail_passes (amount : Nat) : WeakSpec amount alwaysFail alwaysFail :=
  ⟨fun _ => Or.inr rfl, fun _ => Or.inr rfl⟩

structure StrongSpec (amount : Nat) (gatewayOK bankOK : State → Prop)
    (submit settle : Step) : Prop extends WeakSpec amount submit settle where
  submit_ok : ∀ s, s.order = .approved ∧ gatewayOK s → submit s = .ok {s with order := .processing}
  submit_fail : ∀ s, ¬(s.order = .approved ∧ gatewayOK s) → submit s = .error s
  settle_ok : ∀ s, s.order = .processing ∧ bankOK s → settle s = .ok ⟨s.balance + amount, .refunded⟩
  settle_fail : ∀ s, ¬(s.order = .processing ∧ bankOK s) → settle s = .error s

在我实际生产业务的交付模块中，输入对象、输出和执行计划都齐了，决策就必须给出一个后台处理任务，不能返回“无需处理”就结束。

1
2
3
4
5
6

Eligible snapshot
→ 存在 action，
  使 decide snapshot = .enqueue action

decide snapshot = .enqueue action
→ Eligible snapshot

前一个方向由 eligible_decide_enqueue 证明，后一个由 decide_enqueue_sound 证明。还有一条 theorem 保证，拒绝和 eligibility 不成立是同一回事。要发哪个任务也不能随便，输入和执行计划都绑在 action 上，可以被定理检查。

这里展示的不是另写的玩具逻辑，而是生产中的决策逻辑。相关定理验证的，也是生产里用的同一个 decide。拿到 .enqueue action，再交给任务持久化解释器，写进去以后还要核对，任务是不是仍然和这个 action 对得上。

另一个真实案例，同样来自我生产代码库：worker epoch fencing。任务进了终态就不能重新 claim，写 checkpoint 必须拿当前的 exact token。哪怕 worker id 没变，只要重新领过任务，旧 token 就作废。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

def LiveExact (t : Task) (tok : Token) (now : Int) : Prop :=
  t.terminal = false ∧ t.holder = some tok ∧ tok.2 = t.epoch ∧ now ≤ t.leaseExpiry

structure Spec (claim : Task → Nat → Int → Option (Task × Token))
    (checkpoint : Task → Token → Int → Nat → Option Task) : Prop where
  terminal_no_claim : ∀ t w now, t.terminal = true → claim t w now = none
  checkpoint_exact : ∀ t tok now seq t',
    checkpoint t tok now seq = some t' → LiveExact t tok now
  claim_new_epoch : ∀ t w now t' tok, claim t w now = some (t', tok) →
    t'.epoch = t.epoch + 1 ∧ tok = (w, t'.epoch) ∧ t'.holder = some tok
  old_token_fenced : ∀ t w claimAt t' tok now seq,
    claim t w claimAt = some (t', tok) → checkpoint t' (w, t.epoch) now seq = none

发邮件也一样。形式化模型可以要求条件满足时函数必须产生 SendEmail action，但邮箱服务商收没收到、邮件进没进对方收件箱，还得在真实世界验证。

6. 反玩具化

不要求形式化覆盖时，AI 会主动设计一些我没要求的功能。可一旦要求形式化覆盖，它就频繁地削减功能，交付能通过验证、却上不了生产的玩具。这也是我在形式化开发中最难纠正的 AI 坏习惯。

今天我们已经习惯于一句话需求扔给 AI，然后看 AI 表演，欣赏 AI 输出的绚丽图形界面和惊艳的动效，甚至 AI 已经能直接生成 3D CAD 模型，还能跟随音乐鼓点制作交互式 MV。直接扔给 AI 一句话，“给我制作一个可交互的黑洞/虫洞”，“把仙剑1，红警2，魔兽3，生化4移植到 Web”，“制作一个功能完善招聘管理系统”等等。

但同样的需求内容，如果只是简单的附加上“使用 Lean4 开发”然后一起扔给 AI，AI 会给你一个不覆盖任何定理验证的软件。即便你打上“覆盖定理验证，禁止滥用 axiom/sorry 逃逸”的补丁，且划分好了可信外部边界，AI 依然会一反常态的输出一个丑陋的交互界面，且不像过去主动实现你没说出口的需求，反而大幅削减你明确指出的需求。

强迫今天的 AI 贯彻形式化验证，最终得到的只会是从头到尾都是可验证的玩具，你没有办法把玩具推到生产。我让 AI 开发一个业务系统功能，用 Java 实现时一张表 30 列，而用 Lean4 实现时这张表只有 10 列，其中 5 列用来保证与其他表的严格关系约束。即便我让 AI 先基于 Java 思维设计，最后用 Lean4 实现，交付时依然发现 AI 把我没有明说的，却又是约定俗成的功能全省了。

甚至在我早期实验阶段，AI 会单独写一个可验证的 stainless 玩具核心来通过验证，而真实生产 scala 代码则是单独写的另一套。并告诉我全部验证通过，所有 VCs 全绿。我仿佛又见到了写第一篇文章时的那个 AI：编译一通过就给我虚空庆祝，点进去一看，遍地都是空函数和 TODO。

无从得知这一行为的根本原因，我猜测是因为：

1. 通过验证作为最强的奖励信号，使得 AI 宁愿放弃“完整”，也要把验证刷绿
2. 毕竟“完整”甚至没能落实到文字
3. 即便落实到文字，自然语言的模糊也给了 AI 偷懒的空间，能简勿繁
4. 也可能是最关键的，在我之前没人这么干过，AI 更没见过 所以对今天的 AI 来说，形式化必须是一套可执行的工作流和方法论，一句话需求会在形式化软件中收获最拿不出手的结果。

后来我又碰上另一种玩具化：AI 把整张表加载成内存里的 List，排序、过滤后再把结果交给接口，而不是像正常的 Web 项目那样，直接用 SQL 的查询条件筛选数据。

生产代码库有这么一段逻辑，列表每一行都单独查 telemetry；页面只有 50 行，就发 50 条 SQL。还有路径一项一项读、一项一项写，或者每个 Entry 都把完整 output snapshot 重扫一遍。更离谱的一次是删掉 keyset pagination，理由只有“一个组织的项目足够少”，大约两小时后就回滚了。

我猜测新 sql 查询意味着新增公理，而 AI 为了不增加新的公理选择这种方式。毕竟在我形式化项目里，扩展信任边界，增加公理，是必须提供充分理由的，不然无法通过交叉评审。而在内存 List 上过滤只是当前定理的组合，影响最小化，却是最糟糕的生产实现。

我也不是要把所有 List.filter 都枪毙。按业务 key 取、有明确上限的 snapshot，放内存里根据业务进行二次过滤是合理的。但没上界就全表加载进内存、N+1、反复扫整份数据，是不可接受的。AI 在普通业务开发中明明已经养成了不错的性能习惯，到了形式化领域，却又开始知错犯错。

所以若要避免今天 AI 在编写形式化代码时的玩具化倾向，明确的工作流指导（agents.md）必不可少，人类也需要根据自己需求期望补充软件规格，以封堵 AI 的偷懒路径。

7. 拟像与仿真

验证模型能保证 action 必定会按逻辑执行，却无法保证 action 执行后对现实世界的影响是符合我们期望的。因为现实世界的复杂无法穷尽，所以验证并不能完全替代测试。

拿退款功能来说，我们很容易想当然地觉得，调用了支付网关 API，资金就必然到账。但现实中：

• 支付 SDK 是否使用了正确的 secret key 和签名算法
• 是否填入正确参数，序列化协议与网关要求一致
• 收款账户是否被禁用
• 付款账户余额是否充足，是否预留足够的渠道手续费
• 转账附加信息中包含特殊字符甚至黄赌暴恐

等等，这些都是形式模型无法覆盖的。

这是一个极端的例子，对这个外部复杂系统进行完整的黑盒建模，是一件高投入，收益有限的工作。毕竟短信提供商，邮件提供商，乃至支付网关都是可以替换的。

但数据库，缓存，文件系统，对象存储等重要组件，实现虽然复杂，大部分行为却可以被抽象为 List/Map 模型上的操作。开发者和 AI 都早已习惯于为这些组件编写集成测试以保证最常用路径的通畅性。顺手复用同一批测试输入，让真实组件和形式模型各跑一遍，再对比两边的输出，工作量并不大。还能确保形式模型对真实世界的建模一致性。

所以形式化检查通过后，我还加了一层 differential/deviation check，内存模型和真实 PostgreSQL 跑同一组操作，再对一对 verdict 和能观察到的状态。不然 SQL、decoder、mapping 跑偏了，我可能验证的是一套假的程序逻辑。虽然是集成测试，只跑有限的输入和操作序列，但也能部分作为 PostgreSQL 和模型之间的 refinement proof。

例子中的支付网关也值得进行仿真实验，大部分支付提供商都提供了测网环境，集成测试能在产品部署前暴露出更多问题，其中偏差检查部分也能暴露出对支付网关建模时遗漏的特性，提醒开发者需要补充到形式模型中。

第五篇文章中我对测试的预言，在这三个月验证下来基本上是成立的，且实战经验更细化了测试的分工与组织。 纯粹的单测，我 lean 项目里已经很少需要写了，只有系统接口、PG 接口这些交界的地方需要集成测试，业务相关函数模块都不用再写一遍单测。

在基于符号的形式模型进入真实的复杂世界之前，仿真测试的重要性不可替代。

8. 革命不是请客吃饭

这是一个有点长且坎坷的故事

最开始，我尝试和平演进

从生产 Scala 代码出发，对所有外部副作用（数据库、云服务）进行公理化建模，对使用到的三方库函数也做形式化翻译。 生产代码继续写 Cats Effect，并设计了一套 annotation DSL，给业务代码辅助标记 refinement type，和 pre/post-condition。 这样一来我可以自己写一个编译器（翻译器），解析 TASTy 的脱糖 Scala AST，然后生成合法的 stainless 语法。 但是进展非常缓慢，形式化是一个语言子集，永远追不上生产代码的进化速度。并且业务系统中使用到的高级编程技巧，在这一阶段成了巨大的阻碍。

就连基本数据类型也在阻碍我顺利翻译，在形式化领域，使用无上限的自然数类型是惯例，而实际业务系统都是有上限的 Int32/Int64/Float32/Float64，形式化对这些有上限的数据类型，以及 IEEE754 浮点数都需要专门的 BitVectors 运算规则才能表达。对外行来说非常反直觉的是，尽管 BigInt 在计算机里比基础数据类型要慢得多，无上限的自然数在形式化验证时运行更快。（约束条件少）

Scala 中的 IO[A] 同时具有管理资源释放，取消和安全取消，结构化并发等能力，常用的 for-comprehension 语法糖在 TASTy 被翻译成 nested flatMap 。 所以我自己写了一个 FVIO[A] 来作为验证侧的模拟 IO[A]。

我本以为，大量使用 Tagless final 会让形式化翻译器更好写。实际做下来才发现，在形式化这边，它还不如直接用函数传参。这套 DSL 给翻译平添了不少复杂度，最后还是得由翻译器把 Tagless final 抹掉。

实验之前我本以为我的 Pure FP 是距离形式化明月最近的水边楼台，实验中却发现，IO[A] 的模型将可变状态隔离在系统之外，同时给验证带来额外复杂度。 我的 FVIO[A] 模型必须扩展成 FVIO[World, A] 才能承载真实业务，而且 World 在每个 proofs 中并不相同。 同时 Scala 一行代码至少 3-5 个 lambda 的特性也加剧了验证时间/空间的劣化。 在验证时我需要假设被验证函数是立即求值的（或可以等效为立即求值），FVIO[World, A] = StateMonad[S = World, A]。我甚至因此放弃了结构化并发，粗暴的在验证阶段假设 f1 join f2 操作是有先后顺序的。

到这里我的 FP 信仰已经开始产生了动摇，我坚守 FP 是为了什么？ 装 B？ 引用透明？如果形式化能带来最终极的透明，所有副作用在形式化中显现，我又何必在 Pure FP 的路上走到黑？ 就这样，我做出了违背祖训的决定，彻底放弃 IO[A] 抽象，全面拥抱 Direct-style algebraic，使用基于 VirtualThread 的 Ox 重写后端系统。形式化翻译器不需要再翻译 nested flatMap，也不需要做 StateMonad 传递，直接将带副作用的语句翻译为 Stainless。

而以上这些还不是和平演进实验中遇到的最棘手的困难。最棘手的是，生产使用了太多语言特性，框架 DSL。这些充满黑魔法的框架，几乎不可能在形式化世界建立对应的模型。而需求到来时永远是先上线后优化，如果生产引入了未覆盖形式化断言的库/框架，那么会直接导致形式化检查失败。可以预见在实际需求交付压力下，附加的形式化是一定会被牺牲的，变成可有可无的累赘。 给生产系统补形式化，就像是给运行中的列车追着铺铁轨，铺铁轨的永远追不上开列车的。形式化门禁必须前置！

后来我不再追赶

我把方向倒过来：直接使用 Stainless 开发可以被形式化验证的代码，再用 transpiler 生成生产 Scala。要在生产代码中使用 Ox 的结构化并发能力，就得先在 Stainless 侧用 @opaque 和 @extern 搭好对应的形式化桥梁。 这样一来除了最外层的进程初始化，HTTP Server 启动，和路由处理的胶水部分在生产 Scala 侧，从 Service 层开始，所有逻辑都使用 Stainless 直接开发。

当然，数据库和外部 SDK 能力也留在 Scala 侧。这回形式化终于进了生产构建。 但 AI 依然没让我省心，我发现了更多的 AI 逃逸路径：

1. 原本应该很薄的 HTTP 胶水层，本应纯转发函数调用的路由，被 AI 越写越厚，甚至在路由函数中直接读写了缓存数据库。
2. Scala 侧的外部能力也在变厚，原本是普通的写入对象存储逻辑，也只声明了这一种副作用，AI 却偷偷地把写入消息队列也混了进去。

这些逃逸路径的共同点是：AI 都在抄让验证通过的近路，而不是老老实实在 Stainless 侧实现并验证副作用。

我甚至还尝试了 flux-rs 和 MoonBit，可惜后天加入形式化支持的语言都有和 Stainless 一样的缺陷，形式化只能覆盖语言的子集，稍不注意就生成出来无法验证的代码。且限制太多，以至于 AI 处处碰壁。

革命不彻底，就是彻底不革命

AI 为什么总是逃逸？因为始终有多条逃逸路线摆在 AI 眼前。 那我干脆破釜沉舟，彻底转向 Lean4，不给 AI 逃逸的机会。总强得过做个监督孩子写作业的老母亲，频繁检查，频繁纠正，频繁心态崩溃。

改成直接用 Lean 4 写生产代码后，我至少得到了以下几点收益

1. 少掉一层跨语言翻译
2. 不再需要纠结可变/不可变
3. 不再为抽象世界模型发愁
4. Lean 4 已经被形式化过的 StdLib 和贫瘠的生态，此刻反而成了优势：AI 失去了大部分逃逸路径。

最后，落地的是我第四节讲过的路线

9. 慢就是快

全面形式化以后，同事抱怨得最多的就是慢：CI 慢，Agent 开发也慢。以前一天能迭代仨版本，现在一个功能有时要跑一天，甚至两三天。

但这不等于形式化把交付拖慢了几倍。前后做的功能不一样，质量门槛不一样，系统规模也不一样。

Theorem 比语义索引更能帮助 Agent 快速定位到实际代码：从命题找到业务决定在哪儿，改 priority、identity 或 retry 时知道哪些性质不能丢，再去翻 Repo、SQL、Rust、前端和日志。领域类型挡非法输入，Lean 编译器查类型和证明，axiom allowlist 挡没登记的信任，真实 PostgreSQL gate 能抓模型和 SQL 对不上的地方。

所以形式化证明在这里起到的作用是约束了软件的形状，让没有长期记忆的agent可以不依赖模糊的，容易漂移的自然语言文档/spec。而是依赖更清晰，无歧义的定理。

哪怕是开发第一版软件，它也可以展现出价值：第一版不等于 AI 一次生成即正确，通常还要经过数次 commit，数小时甚至数天的迭代；涉及多 sub-agent 协作，跨越多次上下文压缩。所以形式化在这时就能发挥作用，它会拖延你看到软件雏形的时间，却能在长开发任务中帮助 agent swarm 不偏离软件原始目标，同时留下宝贵的形式化软件规格。

形式化验证通过约束软件的核心形状，帮助 AI 更快地分析软件的核心目的，即便跨越上下文压缩，定理也不会被扭曲，因此形式化验证为从量到质的转换提供了强有力的支持。

慢下来的是每个功能 AI 的开发速度，但部署交付后几乎没有 bug，也不会破坏掉已有功能，这反而给整个产品省下了大量擦屁股的时间，也减少了未来需求变更的开发时间。

10. 可再生软件

过去人类写软件的时候，初次编写时就会考虑非常多额外设计，留下宽裕的架构。如果这里要多支持其他存储介质怎么办，要允许其他格式输入怎么办，以至于第一版就加通用抽象、扩展点、兼容层和设计模式，先把复杂度的成本支付了。结果，大部分软件直到生命周期结束，也没等来预想中的第二种变体需求。反倒是那些没留扩展入口的模块，被提了一堆变体需求。

本民科在这里爆论：AI-native 时代将推翻开闭原则。

开闭原则为什么存在？因为修改别人（甚至是数月前的自己）写的代码更容易引入错误。 那现在都是 AI 维护，开一个新 Session 就是新 AI，还需要什么开闭原则？在软件目标发生变化后，对修改关闭的代码，不就是遗留屎山么？

当代码的主要作者变成 AI 后，编写代码也从智力密集型任务变成了算力密集型任务。 如果软件的形状可以被形式化精确记载，那么 AI 也不再需要为尚未出现的需求预留扩展点位。待第二种变体需求真的被提出来后，再从新的合成目标出发重写受影响的模块。

11. 不妄语，梦幻泡影空虚

这篇里出现的人机交互方法肯定只是过渡。以后流行的也许是 Lean，也许不是。编程语言可能会内置更多可检查的契约，也可能出现 AI 时代原生的形式化语言。到那时，人也不必总盯着 AI 漏了多少边界、偷了多少懒。

我希望数据库结构和验证模型能从同一份 DDL 定义生长（生成）出来，而不是手动维护两套，甚至以后不必拘泥于 SQL 还是什么语法范式。

我相信，未来形式化会越来越流行，当下的 AI 需要 harness，而形式化也是应用软件开发领域最好的 harness。

今天的 AI 在应用层软件使用形式化方法还不习惯，还需要许多来自人类的指导。毕竟世界范围内应用层软件使用形式化的先例几乎没有，模型也没有在这上面加强训练过。这些习惯可以通过 RLVR 训练进模型，让拆解定理、保证定理覆盖成为模型的偏好，而不是只靠 prompt/context 许愿抽卡，指望 AI 履行 agents.md 中的形式化宣言。

我想要的“双向奔赴”大概是这样：

• 专门设计一种面向 AI 的编程语言，工具链提供能力，让命题、契约、信任声明都能单独检查，让 kernel 或 solver 拒掉不满足约束的候选
• 专门训练模型，直接在这门 AI 专用的形式化语言上训练，把这些工程选择训练成 AI 的偏好

期待张宏波老师和梁文锋战略合作一下。

面向 AI 的编程语言，不应该只方便 AI 生成，局部的 pass 和 token 最小化对工程质量极可能是负面的，语言设计不应该迁就模型现在的能力。 我的意见正相反：同样的钱能买到越来越聪明的模型，就该让它交出更高质量的代码，溢出的智力（算力）可以转化为软件的质量。 我相信大家都体会到了：1B token 能生成出来的功能，砸进去 10B token 却不会得到 2 倍的功能，或减少一半的 bug。

但如果把 token 砸进形式化里呢？

更重要的是，形式化的应用门槛已经降下来了。不需要博士文凭，没系统学过 Lean 的普通业务程序员，甚至大专、培训班码农，也能借助 AI 开发、维护形式化软件。

过去只有那些关键系统会用形式化方法开发。有的也只是抽出一个核心模型来验证，真正运行的代码仍用业务语言编写。而 AI 带来的门槛降低意味着所有应用都可以一定程度上覆盖形式化验证，不分高低贵贱，火箭飞控，或者是键盘撒把米鸡都会写的 CRUD。

从手写代码、图形化编程、低代码、无代码，到现在 AI 编程，谁也没能解决软件长期开发和维护的问题，当然我也不敢说本文提出的方案能把这事解决了。 我的实验证实的是，AI + 形式化 将已知下界往前推了一步。

无奖竞猜

本文标题《民(科)用广义 Curry-Howard 证明搜索与程序合成器》指的是谁？

• A: 我
• B: Lean4
• C: 本文主张的工作流
• D: 理解并执行该工作流的 AI

勘误

文中出现的所有 lean4 代码均为演示用途的伪代码，经过大幅缩减以适合嵌入到文章内，不是可以直接运行的代码。

很遗憾，本文没有给出受控对照和可复核的量化评估，所以只是一篇“民科檄文”，难登大雅之堂。

一方面，我这支初创草台班子团队，承担不起两条路线并行开发同一套业务的成本。拆分人手、重复开发、收集可比较的数据，都会挤占实际交付的时间。应用软件的需求会变，人员和业务条件会变，市场机会也不会停下来等我做实验。即使改成纯 AI 的对照实验，实验框架和 token 开销也仍然需要投入。实践中观察到的改善，已经足以让我决定背水一战，推广到整个团队。

另一方面，软件质量也很难由几个脱离业务条件的数字概括。

• 代码行数？写得更多，不代表软件更好。
• 运行时故障率？没有多少用户、没有多少实际流量，低故障率能说明什么？
• 圈复杂度？复杂度下降，是逻辑变清楚了，还是必要的功能和边界处理被删掉了？
• bug 数？先统一什么算 bug、怎样发现 bug，再比较数字。
• feature 开发速度？做的是同样难度的需求吗？后续返工和修 bug 的时间算进去了吗？

所以，我能留下的仍然是一个带着“俺寻思”味道的经验结论：在这几个月的实践中，我观察到 bug 明显减少，已修复的问题也较少反复回归，其中包括前后业务规则互相冲突的那类 bug。代码库的膨胀速度放缓了。随着存量代码增加，后续需求的交付时间没有明显拉长，交付质量也没有明显下降。

如果你有低成本开展对照实验的思路，欢迎在评论区交流。