Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper performs a formal verification study of code generated by seven LLMs across 500 security-critical prompts using the Z3 SMT solver via the COBALT analysis pipeline. The study reveals that 55.8% of generated code artifacts contain at least one formally proven vulnerability, with GPT-4o leading at 62.4% and Gemini 2.5 Flash performing best at 48.4%. The authors also found that explicit security instructions have minimal impact, industry tools miss most vulnerabilities, and models generate vulnerable code by default despite being able to identify vulnerabilities in review.
Despite being able to identify vulnerabilities in review, LLMs generate vulnerable code by default more than half the time, and even the best model still produces vulnerable code nearly 50% of the time.
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 frontier 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.