AI 证明了你的代码正确。它实际上证明了什么？

Anthropic 与 Theorem 合作验证了 123 个库中的 239 个入口点，确保在 64 MB 输入限制下无崩溃，基于 RISC-V、Linux 和内存假设。GitHub Next 与微软研究院探索使用 Verus 工具检查 Rust 实现是否符合数学规范，结合测试与人工审核。AI 可生成证明，但验证结果依赖于定义与假设，无法覆盖所有未测试的输入情况。