一个 AI 用了一周时间，把整个底层压缩库 zlib 彻底重写了一遍

一个 AI 用了一周时间，把整个底层压缩库 zlib 彻底重写了一遍。 它没有提交任何单元测试。 它交出来的是整整 32,000 行纯数学证明。 一个只有几千行代码的独立微内核，把每一行逻辑从头到尾验算了一遍。 全部通过。 很多人聊起 AI 编程，焦点全在模型写代码有多快、能写多少行。 真正的致命危机发生在另一头。 当自动化编程代理每周向代码库倾倒成千上万个合并请求时，软件工业现有的所有质检手段，全部失效了。 让大模型给代码打分，本质是概率猜概率，两层幻觉相互掩盖。 单元测试只能覆盖工程师预先想到的边界，测不到没想到的死角。 人工代码评审的精力，在机器每秒几千行的吞吐量面前，连零头都接不住。 三套传统防线加在一起，没有一套能向你保证：这段代码在面对所有可能输入时，绝对没有漏洞。 如果连写代码的人都无法验证结果，成倍暴涨的 AI 生产力，到底是在创造资产，还是在疯狂堆积灾难？ 要解开这个死结，必须把软件工程沿用了半个世纪的分工彻底掀翻。 这台机器叫：形式化验证与规约所有权。 它的核心载体，是正在硅谷重构代码底座的交互式定理证明语言 Lean 4。 过去写软件，人类既要费劲写业务实现，又要写一堆测试用例去碰运气。 在这套新体系里，人类退守到了唯一不可替代的位置：定义形式化规约。 人类只用严格的数学逻辑写下系统的铁律：解压后的输出，必须与压缩前的输入完全恒等。 怎么写出实现代码，怎么证明代码在所有情况下都满足这条铁律，全部交由机器解决。 AI 在背后的推导过程，就像在一张无限大的棋盘上下棋。 它把庞大的最终定理拆解成成百上千个微小的引理。 每推进一步证明策略，就尝试闭合一个逻辑分支。 一旦推导陷入死胡同，立刻自动回溯换路，直到所有分支全部被推导至终局。 AI 生成的这三万多行证明代码，被送进一个精简的独立验证内核。 这个内核完全开源，代码量极小，不包含任何大模型黑箱。 它只做一件事：用确定性的类型论规则，做纯粹的符号验算。 只要内核判定通过，这段代码在数学意义上就是绝对正确的。 不是在一百万次抽检里碰巧没报错。 是在无穷无尽的输入空间里，从数学逻辑上断绝了一切出错的可能。 这套机制早已走出了学术论文，变成了支撑顶级云厂商运转的工业流水线。 AWS 的开源权限系统 Cedar，已经在生产环境里全天候运行这套逻辑。 Cedar 的核心授权语义全部用 Lean 4 编写规约并完成数学证明。 真正上线跑业务的高性能代码，则用 Rust 编写。 每天晚上，AWS 的自动化测试集群会在两者之间狂跑 1 亿次差分测试。 只要 Rust 生产代码的运行结果和 Lean 4 的数学规约出现一丝一毫的偏差，版本立刻被拦截，一行代码都不准发布。 过去几十年，程序员把绝大部分生命耗费在把人类语言翻译成机器指令上。 验收依赖于有限的抽样用例，以及注定会疲劳的人肉眼球。 当 AI 让写代码的边际成本归零，代码本身就降级成了廉价的推论副产品。 真正决定系统生死和商业价值的，只剩下了人类写下的那一纸数学规约。 未来的软件构建，不再是人教机器怎么写逻辑，再祈祷测试跑通。 是人类锁定数学真理的边界，机器在里面完成穷尽证明。 当代码能够被数学证明的那一刻，软件才真正从一门碰运气的经验手艺，变成了精密可靠的现代工程。