验证方法形式化证明与全量验证各自保证什么。结构待定：本栏目的结构仍在讨论中，下列子页只是占位，标题和划分都可能调整。 形式化证明复制锚点链接 待写：说明 Lean 证明覆盖的范围。 全量验证复制锚点链接 待写：说明全量验证覆盖的范围，链接到报告第二部分。Lean 定理对照表报告中的定理与 Lean 形式化证明的对照。