【形式化验证：从昂贵的“学术玩具”到大模型时代的“标配”】最近 Adam Langley 用 Lean 语言实现 Zstandard 解压器的实验引发热议。核心事实是：长期以来，形式化验证（Formal Verification）因其成本极高（通常是开发成本的10-20倍）而仅存于航空航天或微内核等极端场景。但现在，LLM 展现出自动生成 Lean 证明代码的惊人潜力，原本需要专家耗费数周的复杂证明，AI 可能在几十分钟内搞定。这意味着我们可以用机器检查代码中的每一个细微变元，让“代码即证明”真正落地。这标志着软件工程底层逻辑的范式转移。过去我们靠测试发现 Bug，但测试只能证明 Bug 存在，不能证明其不存在；而形式化验证通过数学逻辑锁定程序的边界。虽然有人担心这只是把 Bug 从代码挪到了“规格说明（Spec）”里，或者 LLM 会一本正经地证明错误的功能，但不可否认的是，当证明成本大幅下降，程序员的核心技能将从“写具体实现”转向“编写严谨的规格说明”。这不仅是安全性的飞跃，更是 AI 时代硬核编程的新门槛。 imperialviolet.org/2026/07/26/zstd-lean.html