# Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code

arXiv: https://arxiv.org/abs/2604.05292 · HTML: https://mlsanity.com/paper/2604.05292/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 16 references that are in the map.
- First posted on arXiv 7 Apr 2026.

## Builds on (most cited first, 6 of 6)

- [Large Language Models](https://mlsanity.com/paper/2307.05782/) (2023)
- [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021)
- [Do Users Write More Insecure Code with AI Assistants?](https://mlsanity.com/paper/2211.03622/) (2022)
- [Large Language Models for Code: Security Hardening and Adversarial Testing](https://mlsanity.com/paper/2302.05319/) (2023)
- [Lost at C: A User Study on the Security Implications of Large Language Model Code Assistants](https://mlsanity.com/paper/2208.09727/) (2022)
- [LLMSecEval: A Dataset of Natural Language Prompts for Security Evaluations](https://mlsanity.com/paper/2303.09384/) (2023)

## Built on by (most cited first, 1 of 1)

- [Automating Formal Verification with Agent-Guided Tree Search](https://mlsanity.com/paper/2605.27485/) (2026)

## Abstract (arXiv)

AI coding assistants are now used to generate production code in security-sensitive domains, yet the exploitability of their outputs remains unquantified. We address this gap with Broken by Default: a formal verification study of 3,500 code artifacts generated by seven widely-deployed LLMs across 500 security-critical prompts (five CWE categories, 100 prompts each). Each artifact is subjected to the Z3 SMT solver via the COBALT analysis pipeline, producing mathematical satisfiability witnesses rather than pattern-based heuristics. Across all models, 55.8% of artifacts contain at least one COBALT-identified vulnerability; of these, 1,055 are formally proven via Z3 satisfiability witnesses. GPT-4o leads at 62.4% (grade F); Gemini 2.5 Flash performs best at 48.4% (grade D). No model achieves a grade better than D. Six of seven representative findings are confirmed with runtime crashes under GCC AddressSanitizer. Three auxiliary experiments show: (1) explicit security instructions reduce the mean rate by only 4 points; (2) six industry tools combined miss 97.8% of Z3-proven findings; and (3) models identify their own vulnerable outputs 78.7% of the time in review mode yet generate them at 55.8% by default.