Tags: #形式化验证

讨论 Lean 如何为 AI 生成代码提供可检查的规格与证明，并厘清它与 Rust、测试及真实实现之间的能力边界。