Three ways formally verified code can go wrong in practice19 hours agohttps://buttondown.com/hillelwayne/archive/three-ways-formally-verified-code-can...正式验证的代码仍可能存在缺陷，若证明本身无效，例如定理证明器中的错误或使用未经证实的假设（捷径）。当被证明的属性（规格说明）错误或弱于需求时会出现缺陷，如左填充示例证明字符串长度而非Unicode视觉对齐。即使证明有效，假设（如环境条件或未经验证的依赖项）也可能破坏正确性，如二分查找溢出问题或依赖外部服务的情况。