加载失败
讨论基于一篇题为“How to train your program verifier”的文章展开，作者据称借助 LLM 生成数学或规范并用于训练/驱动程序验证器（program verifier）。批评者把注意力放在文章示例上，指出若缺乏路径可达性证明就无法确认被标记的“bug”是真实可触发的，评论中引用了 Python 的 requests（HTTP 客户端库）示例，提到 address_in_network 与 is_valid_cidr 的调用顺序。讨论涉及静态分析、symbolic execution（符号执行）、tainting/可达性分析以及以 Z3（微软的 SMT 求解器）为代表的自动定理证明技术的角色，并以 Trail of Bits 博客（安全研究机构）关于 AES-CTR 默认 IV 导致 key/IV 重用的真实案例说明糟糕 API 设计可以带来大规模安全后果。
多位评论者指出，文章列出的“bug”缺乏可达性证明，很多可能只是静态分析的误报。举例指出在 requests 库中被报告的第一个问题实际上在调用 address_in_network 之前由 is_valid_cidr 校验了斜杠，因此那条路径不可达。评论还强调静态分析本身通常采取保守策略，降低 false positive 率需要建模 tainting/可达性或至少做到 1-callsite sensitivity；在这类分析缺失的情况下把误报当作成功是误导性的。总体观点是：没有可达性/污点模型的结果不足以支持“有效验证”之类的强声明。
另一组评论认为工具指出的问题有现实意义，因为函数可以被直接错误调用，问题源自 API 设计或文档不明确而非分析器的单方面失误。有人建议如果 B 必须在 A 之后调用，要么让 B 自行做验证，要么让 A 返回一个 token 强制调用顺序，否则安全性被寄托在调用者的“正确使用”上。也有不同意见认为抛异常是可接受的（比如 math.sqrt 对负数抛错），但反面例子被提出：Trail of Bits 博客指出 aes-js 与 pyaes 在 AES-CTR API 中提供默认 IV 导致大量 key/IV 重用，表明糟糕的 API 设计会导致大范围安全问题。讨论围绕到底是“文档问题”还是“设计问题”展开，并提出若要称为已验证代码应消除此类易错表面。
也有评论强调形式化验证的正面价值：被证明正确的代码可以省去许多运行时检查，从而提升性能并减少维护负担。支持者指出，验证使得编写看上去“危险”的精简代码成为可能，因为证明能替代冗余的防御性检查，并且编译器/工具会在可证明安全时删除 bounds 或类型检查。与此同时，批评者提醒说既然宣称做了验证，就应更严谨地展示证据——验证不是为了制造安全幻觉，而是要能证明对不变式和可达性的严格处理。
不少评论对文章的来源与质量表示怀疑，认为这是 LLM 快速生成的长文而非经过严谨人工验证的研究，作者对生成结果过于轻信并夸大其意义。有人嘲讽把 AI 要求写出“Voevodsky 级别”的数学而又不加“别出错”的约束是荒唐的，并且讽刺文章中诸如“不要只问系统是否安全，而应问它离安全有多远”的伪深刻表述。整体语气是对 LLM 带来表面可读但空洞论述的不信任，呼吁对验证结果和示例进行更严格的人类审查与可达性证明。
program verifier: 把程序与形式化规范关联、使用逻辑推理或自动定理证明器（如 SMT solver）证明程序满足规范的工具或系统。
static analysis / static analyzer: 在不运行程序的情况下分析代码以发现潜在错误的技术，通常采取保守近似，会产生 false positives，需要可达性或上下文敏感性策略来降低误报。
symbolic execution: 用符号值代替具体输入执行程序以穷举路径并生成约束条件的方法，常配合 SMT solver 求解路径可达性或生成反例。
tainting / reachability analysis: 跟踪不可信输入（taint）如何传播并判断某条路径或错误是否可达的分析技术，能显著减少静态分析报告的误报。
SMT solver / Z3: SMT（Satisfiability Modulo Theories）求解器用于判定逻辑公式是否可满足；Z3 是 Microsoft Research 的著名 SMT solver，常被程序验证工具作为后端。