三种在实践中可能出错的正式验证代码方式

本文探讨了即使经过形式化验证的代码仍可能出现错误的三种情况：证明本身无效、规范属性错误、以及基本假设错误。作者通过"左填充"函数验证失败的案例，揭示了形式化验证中"正确性"概念的模糊边界。