Anthropic 汇编级形式验证引热议，ezyang 追问 TCB
Anthropic 与 Theorem 合作发布研究：用 Claude 为 100 多个真实开源软件库在 RISC-V 汇编层面证明安全性质，据称是首个在汇编级对生产软件大规模应用 AI 形式验证的尝试，写证明过程中 Claude 还发现了真实缺陷。这一成果引发了 ezyang 对形式验证可信基座（TCB）的连续追问：结论未必错，但「验证可信度取决于你信什么」这一层被系统性低估。
已确认
- Anthropic 发布与 Theorem 合作的汇编级形式验证研究，规模为 100 多个开源软件库，验证层面为 RISC-V 汇编。
- ezyang 指出规格语言越花哨风险越大：堆更多语言特性、依赖可信的 elaboration 或元编程机制生成规格，都会扩大 TCB，增加规格本身出错的风险。
- 他以 C 编译器为例说明 UB 的反直觉行为：条件之后出现 UB 时编译器可假设该条件恒为假，因此即便复用编程语言本身当规格语言，最好也对规格证明无 UB，否则底层编译语义会悄悄破坏验证结论。
- 用编程语言直接写性质（如 Anthropic 文中「不许崩溃的 fuzz test 程序」）可绕开专用规格语言，但代价是编译正确性也进入 TCB。
尚未确认
- ezyang 提出的开放问题尚无答案：用户要求用 Python 写规格时，如何弥合 Python 与形式化语义的鸿沟；若用 vibe-coded Python 脚本把程序 trace elaboration 成 Lean，这个 TCB 该信多少；反过来给 Python 写形式语义又是否可行。
为什么重要
- 这是 LLM 时代形式化验证落地的核心难题：AI 能量产证明，但证明的可信度仍受限于规格语言、elaboration 管线与编译器语义构成的 TCB。ezyang 的质疑提醒业界：验证链条上每一层「顺便信了」的东西，都可能成为整个结论的薄弱点。
2026-11-09 ~ 2026-11-09 · 6 条相关
一手来源
- Anthropic 用 Claude 给 100+ 开源库做汇编级形式验证，ezyang 提出 TCB 之问 — ezyang ·
- ezyang：规格语言功能越花哨，验证的可信基座风险越大 — ezyang ·
- ezyang：用编程语言本身当规格语言，编译正确性也进了 TCB — ezyang ·
- 【源头】Anthropic 用 Claude 给 100+ 开源库做汇编级形式验证，ezyang 提出 TCB 之问 — ezyang · 2026-11-09
- 【源头】ezyang：用编程语言本身当规格语言，编译正确性也进了 TCB — ezyang · 2026-11-09
- ezyang：编译器 UB 陷阱提醒你——规格也要证明无未定义行为 — ezyang · 2026-11-09
- 【源头】ezyang：规格语言功能越花哨，验证的可信基座风险越大 — ezyang · 2026-11-09
- ezyang：用户要 Python 写规格时，形式化鸿沟怎么补？ — ezyang · 2026-11-09
- ezyang：让 LLM 把 Python 程序转成 Lean 证明，这条管线可信吗？ — ezyang · 2026-11-09