把可验证代码从 1% 缩到全集：形式验证的现实困境

jd_pressman · x · 2026-10-23

jdpressman 与 lusichu 讨论形式验证的实际难度：如果从内核开始强制验证，会破坏所有下游软件的兼容性；如果坚持兼容性，就被迫使用难以证明的编程模式。但他强调，即便部分实用模式无法验证或无法替换为可验证等价物，把搜索空间缩小到只剩这些程序仍是巨大进步——这类代码可能只占 1%。

在另一条回复中他指出，我们对形式验证「不可行」的直觉可能是过时的缓存印象：自从它作为通用方法被放弃以来，学术界在形式验证与工具链上一直在稳步进展，只是过去人力成本太高而难以实用。