一句话结论：把 Go 源码翻译成数学方程，用 Z3 约束求解器证明某条边界路径可达，再用 go test 重放崩溃输入确认——这条「用数学抓模糊测试漏网之鱼」的路子，Google 已经真跑通了。
模糊测试一直是找 bug 的主力，但它本质上是瞎蒙输入。Google 这次换了个思路：不猜输入，而是把代码本身变成方程，直接问求解器「这条绝大多数人想不到的边上，到底能不能崩」。
模糊测试：效率高，但靠运气
先说模糊测试（fuzzing）的原理。它随机生成、变异输入去喂程序，一惊一乍地撞出崩溃。覆盖率越高，撞到问题代码的概率越大，所以它平时守着「随机 + 变异 + 覆盖率反馈」的打法，确实能挖出一堆边界问题。
但它的本质是采样式搜索：生成一万个输入，可能只有一两个踩中那条极小概率的分支。所以模糊测试从不敢拍胸脯保证覆盖，只能说这一万次运气还不错。
说白了，模糊测试的问题是「盲区」。它对数值上很难命中、逻辑上很绕、但真实存在的程序状态，往往怎么打都够不着。覆盖率高不等于没有死角，只是死角被照到得少而已。
Z3 登场：从「瞎蒙」到「解方程」
Z3 是微软研究院开源的 SMT 求解器，办的是约束求解的活。给它一堆约束方程，它能告诉你：这些条件同时成立时，变量该怎么取值；或者干脆判定「无解」。
类比一下你写代码时的直觉：fuzzing 是在门口猜钥匙，Z3 是直接把锁结构摊开，算出哪把钥匙能开。它不靠碰运气，而是按数学规则把可达路径算出来——只要约束不冲突，就给出可行赋值。
所以让 Z3 盯边界 bug 很自然：你在代码里画一条「想都不敢想」的路径出来，转化成方程，剩下的交给求解器证明它到底通不通。
流程拆解：源码、反汇编、约束、重放
这次演示的完整链路是这样：先把 Go 源码和对应的 RISC-V 反汇编都拿来，当作「同一段语义的两种写法」；然后由模型把它们翻译成 Z3 约束方程。
翻译的关键在于「语义对齐」。源码表达的意图、反汇编表达的机器行为，两条线要合流成一组约束，求解器才能在一个统一的空间里找这样的输入值：它能同时满足这段路径上的所有条件。
约束有了，接下来是验证而不是轻信。把求解结果作为输入重放：真的跑一遍 go test，用崩溃输入证明「这段路径确实会崩」，而不是求解器口嗨。这一步把「数学上的可能」落回「实际运行的真实」。
这里划重点：整个环节里生成约束的是模型，判定可达并给反例的是 Z3，最后拍板真实崩溃的是真实运行。三件事分开，谁都不能越权。
为什么是「LLM 翻译 + 求解器证明」
这是我的第一点判断：这个组合比单用任何一方都强。模型的优势是读代码、抓语义、把抽象意图说出来；求解器的优势是能计算、能证明、能给出确定的答案。让模型翻译、让求解器证，正好扬长避短。
单用大模型找 bug，它靠的是训练数据里见过的「相似崩溃」，猜测成分重，而且很难给出可复现的输入；单用静态分析工具，又经常被程序状态爆炸和复杂约束卡死。两者套起来，才把「可能的 bug」升级成「被证明可达的 bug」。
还有一个隐蔽的好处：反汇编和源码一起喂，等于强制求解器同时受「程序想干什么」和「机器实际在干什么」双重约束，覆盖面比只看源码宽。对真实世界中编译器优化造成的错位，这种双通道更扛得住。
顺便说一句，这次演示背后是 Google agent skills 项目的负责人，同批还开源了一个检查 SKILL.md 的 Go CLI 工具 skill-lint。同一个团队一边做形式化验证，一边给 agent 技能描述做静态检查，口味相当一致。
前提与边界：Z3 不是银弹
但这里有个前提——第二点判断：Z3 不是万能的，程序状态一爆炸它就解不动。约束越多、变量范围越大，方程就从「好解」滑向「装不进内存」，求解时间也可能从秒级涨到没边。
所以它真正擅长的是「小而深」的问题：几条边界路径、几个关键变量，约束少而精确。真要拿它去解一个亿级状态的真实模块，多半会卡在可扩展性上——规模就是那条隐藏的水位线。
模型的翻译质量也是隐形成本。把语义翻译错，等于给求解器喂了错误方程，Z3 再厉害也证明不出你想要的结论。所以演示里那步「go test 重放、落回真实运行」，恰恰是给翻译层兜底的存在。
我的结论是：这条路的价值不在替代 fuzzing，而在补它的盲区——一个靠运气、一个靠证明。今后写 Go 或任何带边界约束的代码，把这类工具当作「第二个评审人」放进流程，比指望它接管全部测试更务实。
不过说到底，能翻译、能证明、还能回放验证，这套「模型 + 形式化方法」的配方正在把程序分析从经验主义往数学化那边推。留给我们的问题也变了：当代码越来越难翻译成约束时，谁来做语义兜底？
