seL4 的复盘报告留下两个数字:证明耗时是设计加实现的10倍,证明代码行数是C代码的20倍。这是依赖类型编程小众三十年的账本——不是这套类型系统不够聪明,是普通团队请不起这笔证明工时。
最近有工程师换了个思路:用LLM在Lean里辅助写一个Zstandard解压器的证明,再丢给Lean的类型检查器去校验。这只是一个人的实验,没有发布会,也没有性能数字。但它戳中了一个真问题——形式化验证卡住的到底是"证不出来",还是"证不起"。
实验做了什么,又留了哪些空白
- 对象.选Zstandard,是因为它的格式和FSE熵编码足够复杂,能测出Lean是不是真扛得住系统代码,而不只是玩具题。
- 分工.LLM写证明草稿,Lean的类型检查器拍板通不通过。证明成不成立,机器说了算,不是模型自己说了算。
- 空白.作者没公布成功率、耗时、证明规模,也没说清人工介入了多少。他明确说这只是"有限测试",不是结论。
有一个坑作者自己提过:花了很长时间证明,最后发现要证的命题根本是假的。这种"白干"在依赖类型编程里是常态,LLM目前也没能帮着提前避开。
旧瓶颈换了道具,没有消失
依赖类型语言有个优雅的性质:证明写对了,内容本身不重要,只要它存在。麻烦在两处:代码一改证明就要重新对齐,费时费力;复杂证明还可能把类型检查器直接拖到内存爆炸。
业界之前也试过自动化,比如F*让SMT求解器自动消化证明义务。简单情况好使,复杂情况求解器容易一头扎进去转半天出不来。用惯这类语言的人练出一种"六感"——什么写法能讨好求解器,照着套路写。这套自动化,把工程问题变成了半个玄学。
LLM带来的变量,是把"证明内容不重要"这条性质用到极致:反正只要有证明,让模型写草稿,类型检查器把关,分工天然。作者说在他有限的测试里,LLM至少没把类型检查器炸掉。但这只是一个人的经验,能不能推广到更大规模的证明,还看不清。
谁该现在跟进,谁不必
| 领域 | 现在该做什么 | 原因 |
|---|---|---|
| 密码学、协议实现团队 | 可以小范围试点 | 正确性要求高,长期请不起专职证明团队 |
| 编译器、安全关键基础设施 | 可以小范围试点 | 证明成本是长期痛点,ROI 明确 |
| 普通业务开发 | 不必现在跟进 | 本来就不打算形式化证明,收益有限 |
规格写错这件事,LLM帮不了。命题本身错了,证明再漂亮也是白证。这个责任还在人身上。
锐评:省的是力气,不是信任
真正要判断的不是LLM会不会写证明——它已经能写。要看的是这条流程能不能把形式化验证从少数人的手艺,变成可以规模化的日常工程。
可信链没有变短。LLM生成的证明,最终仍要过Lean内核这一关。价值在于把体力活外包出去,不是让模型成为可信根。
类型检查器资源爆炸、代码变更后的证明维护,这两个老问题都还在。LLM目前只解决了"谁来写草稿"。
接下来最该盯的变量,是有没有更大规模、更多人参与的复现——证明规模上去之后,LLM生成的草稿还能不能过关,维护成本会不会反弹。一个人的有限测试,还撑不起"形式化验证已经工程化"这句话。
内核认的是证明,不是模型;省下来的是力气,不是判断力。