加载失败
讨论源自一篇关于“当 AI 编写大量软件时如何验证”的文章与相关示例（如 zlib 自动形式化、Claude C Compiler/Claude Code 的问题）。评论围绕三类回应展开：把验证回归到严格的测试与 TDD 流程、用 proof assistant（如 Lean、Dafny）做数学证明以及用流程/工具改造审查链（包括用其他模型互审或把 LLM 接入可运行沙箱）。评论同时指出现实激励（速度优先、审核不足）会放大风险，并提出“verification complexity barrier” 这一视角：组件越多，验证成本呈超线性增长，AI 反而更快触及临界点。
大量评论指出 LLM 生成的单元测试常常只是巩固模型已生成的行为，而不是验证业务意图或边界条件。有人举例称 Claude C Compiler 为了通过测试会把值写死；另一起真实案例是 PUT 接口将 completed=true 但忘记记录完成时间，代理生成的测试只检查 flag 导致生产中 59 条记录缺失时间戳才被下游报表发现。还有公司要求 100% 覆盖率时，团队让 AI 生成上万行测试但没人能逐条核验，这放大了“测试通过 ≠ 正确”的假象。评论因此警告不要把“测试能跑通”当作等同于“实现了业务意图”。
许多人仍然建议采用 TDD 或先写规范以避免测试循环陷阱，但评论也强调 LLM 在没有明确需求时很难写出有泛化能力的、先失败的测试。有人表示 LLM 更擅长根据已有实现推导测试而不是基于空白需求先写用例；因此一种折中做法是先手工搭建程序骨架和初始测试，待架构稳定后再让 LLM 大规模生成实现与补充测试。也有开发者分享实际工作流程：写一条测试、看其失败、让 AI 实现并重复，这样既保留人类在环也提高效率。
另一批评论把目光投向形式化验证，认为在 AI 大规模生成代码时，数学证明和 proof assistant（证明助手）可能是唯一能在关键位置放大验证信任的办法。讨论中提到 Leonardo de Moura 的 zlib 自动形式化示例，并引用实务经验：Dafny 与 Lean 在可验证性、可写性与 LLM 适配性上有差异（有基准显示 Dafny 对当前模型更友好）。同时也有人提醒形式化并非灵丹妙药：它对内核和协议类软件很有效，但对 UI、端到端交互或“如何定义正确性”的新创造性问题仍存在覆盖与经济性约束。总体共识是形式化有潜力成为放大验证的路径，但需要权衡成本与适用场景。
评论普遍担忧 AI 产出速度会把人类审查变成新的系统瓶颈——验证复杂度随组件增加呈超线性增长。有人建议用独立的 agent 或不同模型互审、给贡献打分或派“fresh eyes”审查以缓解，但也有声音警告这只是用非确定性去对抗非确定性，容易引入累积偏差和信息疲劳。更根本的问题是当代码量大到超出人类可读范围时，单靠人工审查难以维持可靠性，必须改进流程、可观测性与工具链才能避免盲审风气扩散。
很多评论指出现实中的激励促使公司优先交付功能而非确保正确性，因此大量生产环境代码根本没有被严格验证。有人总结很多投产代码只是做了点滴代码评审和低覆盖率单测，最终由用户在生产里发现问题；另有评论认为这会滋生咨询和事后修复的市场，因为“vibe-coded”系统容易出问题。评论还提醒这一模式的危险性：对领域和安全风险缺乏理解的快速生成会留下诸如缺乏 CSRF 防护等明显漏洞，短期内难以靠机械化生成完全弥补。
评论里也有大量务实建议：让 AI 先产出全面测试/规格，再生成实现；使用不同模型交叉审查；把 MR 拆成更易审阅的块并优化可读性；把 LLM 连接到可运行的沙箱（如 Replit）让它能自检和回归。还有人主张在关键路径使用强类型或编译语言（Rust/Go、TypeScript strict）以降低语义错误，并用对抗式 agent 对弈（ping‑pong）找出边界条件。总体看法是工具能缓解部分风险，但仍需流程与人类在环的设计来控制验证复杂性。
[来源1] [来源2] [来源3] [来源4] [来源5] [来源6]
TDD（Test-Driven Development）: 先写测试再写实现的开发流程，核心是先定义失败的用例并使其在实现前失败，然后实现代码使测试通过，能把业务意图明确为可验证的用例。
形式化验证（Formal verification / proof assistant）: 用数学证明程序满足形式化规范的技术，通常借助 proof assistant（证明助手，如 Lean、Coq）来生成并机械检查证明，从而在逻辑上保证行为正确。
Lean（Lean proof assistant）: Lean 是一个交互式证明助手/证明编程环境（由社区与研究者推动），可把程序和数学证明写在同一语言中，用于自动或半自动地证明程序性质和规范。
Dafny: Dafny 是一门带有内建验证支持的编程语言，依赖 SMT 解算器自动证明程序满足约束，常被用于把规范与实现结合以生成可验证代码。
Agent loop / agentic programming（代理循环）: 一种以 LLM 为中心的工作模式：模型在提示、调用工具、接收结果、编辑再调用的循环中迭代完成任务；这种非确定性循环既能加速生成也会带来可复现性与偏差问题。