Anthropic's assembly-level formal verification with Claude draws ezyang's TCB questions

Anthropic, in collaboration with Theorem, published research using Claude to prove safety properties at the RISC-V assembly level for more than 100 real-world open-source software repositories—reportedly the first attempt to apply AI-driven formal verification at assembly level to production software at scale. Along the way, Claude even uncovered genuine defects while writing proofs. The work prompted a series of pointed questions from ezyang about the trusted computing base (TCB) of formal verification: the conclusions may not be wrong, but the layer of "how much you trust determines how valid the verification is" is systematically underestimated.

Confirmed

• Anthropic released the assembly-level formal verification research done with Theorem, covering 100+ open-source repositories, with verification performed at the RISC-V assembly level.
• ezyang points out that fancier specification languages carry greater risk: piling on more language features, or relying on trusted elaboration or metaprogramming mechanisms to generate specs, expands the TCB and increases the chance that the specs themselves are wrong.
• Using a C compiler as an example, he explains how counterintuitive UB can be: if UB occurs after a conditional, the compiler may assume that condition is always false—so even when reusing the programming language itself as the specification language, it's best to also prove the spec free of UB, otherwise the underlying compilation semantics can quietly undermine the verification results.
• Writing properties directly in the programming language (such as Anthropic's "fuzz test program that must not crash") sidesteps dedicated specification languages, but at the cost of pulling compiler correctness into the TCB.

Not Yet Confirmed

• ezyang's open questions remain unanswered: when users demand specs written in Python, how do you bridge the gap between Python and formal semantics; if a vibe-coded Python script elaborates a program trace into Lean, how much should that TCB be trusted; and conversely, is writing formal semantics for Python even feasible.

Why It Matters

• This is the core challenge of putting formal verification into practice in the LLM era: AI can mass-produce proofs, but their trustworthiness is still bounded by the TCB formed by the specification language, the elaboration pipeline, and compiler semantics. ezyang's critique is a reminder to the field: every layer of the verification chain you "trust along the way" can become the weakest link in the entire conclusion.

2026-11-09 ~ 2026-11-09 · 6 related posts

• [source] Anthropic proves security of 100+ open-source libs at assembly level; ezyang asks how much of that TCB to trust — ezyang · 2026-11-09
• [source] Reusing your programming language as a spec language pulls compilation into your TCB — ezyang · 2026-11-09
• Compiler UB gotchas mean your spec itself needs to be proven UB-free — ezyang · 2026-11-09
• [source] ezyang: fancier specification languages quietly grow your trusted computing base — ezyang · 2026-11-09
• If users demand specs in Python, how do you bridge the formalization gap? — ezyang · 2026-11-09
• How much should you trust vibe-coded Python-to-Lean elaboration pipelines? — ezyang · 2026-11-09