形式化验证专家泼冷水：Rocq/Lean 证明通过不等于代码实现了预期功能

形式化验证专家 srchvrs 针对近期多家公司论文宣称的「突破」提出警示：用 Rocq 验证生成代码、用 Lean 检查数学证明，证明通过不等于代码实现了预期功能。他指出形式化验证只保证证明本身被检查器验证通过，并不保证形式化定理真的捕获了原始数学命题，spec 本身的正确性在验证范围之外。