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.

翻译：AI编程助手现被用于生成安全敏感领域的生产代码，但其输出结果的可利用性仍未得到量化。本研究通过“天生缺陷”项目填补这一空白：对七种广泛部署的大语言模型在500个安全关键提示（涵盖五种CWE类别，每个类别100个提示）下生成的3,500个代码制品进行形式化验证。每个制品经COBALT分析流水线提交至Z3 SMT求解器，生成数学可满足性证明而非基于模式的启发式结果。在所有模型中，55.8%的制品包含至少一个COBALT识别的漏洞；其中1,055个漏洞通过Z3可满足性证明得到形式化验证。GPT-4o以62.4%的漏洞率（F级）居首，Gemini 2.5 Flash表现最佳为48.4%（D级）。无模型获得优于D级的评分。七项代表性发现中的六项通过GCC AddressSanitizer运行时崩溃得到确认。三项辅助实验表明：(1)明确的安全指令仅使平均漏洞率降低4个百分点；(2)六种行业工具组合未能检测出97.8%的Z3证明结果；(3)模型在审查模式下能识别自身78.7%的漏洞输出，但默认状态下仍以55.8%的概率生成这些漏洞。