为什么GCC能被验证，而PDF却不行？

Specifications Don't Exist (2025)

文章指出，形式化验证的瓶颈往往不在于证明过程，而在于规格说明的缺失。对于GCC编译器或SeL4微内核，我们拥有清晰的数学定义，验证虽昂贵但可行。然而，像Chrome浏览器或PDF格式这样的系统，由于缺乏精确且统一的规格说明，甚至可以说“规格说明根本不存在”。现实中充斥着大量模糊、矛盾的非正式文档，导致系统行为处于灰色地带。即使未来AI让证明变得廉价，若无法明确“我们要什么”，形式化验证依然寸步难行。