Anthropic 用 Claude 给 100+ 开源库做汇编级形式验证，ezyang 提出 TCB 之问

ezyang · x · 2026-11-09

Anthropic 与 Theorem 合作发布研究：用 Claude 为 100 多个真实开源软件库在 RISC-V 汇编层面证明安全性质，据称是首个在汇编级对生产软件大规模应用 AI 形式验证的尝试；写证明过程中 Claude 还发现了久经数万亿次测试仍未被发现的 bug。

ezyang 借此提出系列追问：为汇编等低级语言写形式语义更容易，但证明需从低级汇编重建高层结构、成本上升；假设语言有形式语义可复用原语言写规格（如把性质写成不许崩溃的 fuzz test），可编译正确性又进了 TCB；编译器的 UB 行为会做反直觉假设，规格也需证明无 UB；最终回到核心难题——如果用户要 Python 写规格，靠一堆 vibe-coded 脚本把 trace elaboration 成 Lean，这条 TCB 到底信多少？