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

This formal verification study demonstrates that AI-generated code across seven frontier LLMs is fundamentally insecure, with 55.8% of artifacts containing mathematically proven vulnerabilities that evade industry-standard tools and persist despite explicit security instructions.

The Gist

Imagine you hire a brilliant, fast-talking apprentice to write the blueprints for your house. This apprentice has read every book ever written, knows thousands of architectural styles, and can draft a room in seconds. But there's a catch: this apprentice has never actually lived in a house, and they learned to build by copying old blueprints that often had hidden cracks.

This paper, titled "Broken by Default," is a formal investigation into what happens when we let these AI "apprentices" (Large Language Models) write code for our digital houses, especially the parts that need to be secure, like locks and vaults.

Here is the breakdown of their findings, translated into everyday language:

1. The Big Discovery: "Broken by Default"

The researchers asked seven of the smartest AI models in the world to write 500 different types of code (like building a password system or handling money). They found that more than half (55.8%) of the time, the AI wrote code that was broken and could be hacked.

• The Analogy: Imagine asking a chef to make 100 sandwiches. If 56 of them have a rock inside, you wouldn't say, "Well, the chef is trying their best." You'd say the kitchen is broken.
• The Grades: Even the "best" AI model only got a D. The top model (GPT-4o) got an F. None of them passed the safety test.

2. The "Magic Glasses" (Z3 Solver)

How did they know the code was actually broken? Usually, security tools are like spellcheckers. They look for bad words (like "unsafe") or patterns they've seen before. If the AI writes a new, clever way to break a lock, the spellchecker misses it.

The researchers used a tool called Z3, which is like a mathematical super-simulator.

• How it works: Instead of just looking for bad words, Z3 tries to solve the math puzzle of the code. It asks, "Is there any number I can type in here to make this crash?"
• The Result: If Z3 says "Yes, here is the exact number," it's not a guess. It's mathematical proof that the code is exploitable. They found over 1,000 of these "proofs."

3. The "Runtime Crash" (The Reality Check)

To make sure the math wasn't just theory, they took the "proofs" from Z3 and actually ran the code on a computer.

• The Analogy: It's like the architect says, "This bridge will hold," but the engineer builds a small model and drives a truck over it. If the bridge collapses, you know it's broken.
• The Result: In 6 out of 7 tests, the code actually crashed or let hackers in. The math was right; the code was dangerous.

4. The "Magic Spell" Didn't Work (Prompting)

People often think, "If I just tell the AI, 'Please be safe and secure,' it will fix itself." The researchers tested this by giving the AI a special "security instruction."

• The Result: It barely helped. The error rate only dropped by 4 points.
• Important Context: This specific test was run on a smaller 50-prompt sub-corpus (a subset of the full 500-prompt benchmark). While the scale was smaller, the result highlights a critical truth: a simple reminder doesn't fix the core problem.
• The Analogy: It's like telling a person who has never learned to swim, "Please don't drown," and then throwing them in the deep end. They still can't swim. The AI's "muscle memory" for writing code is so used to the old, unsafe ways that a simple reminder doesn't fix it.

5. The "Security Guards" Are Asleep (Static Tools)

The researchers tested the industry's best security tools (the "guards" that usually catch bad code) against the AI's output.

• The Result: These tools missed 97.8% of the broken code that Z3 found.
• The Analogy: Imagine a burglar breaking a window with a brand new, invisible tool. The security guard is looking for a crowbar or a lockpick. The guard sees nothing and says, "Everything looks fine!" The guard isn't stupid; they just aren't looking for the right kind of danger.

6. The "Amnesia" Effect (Generation vs. Review)

Here is the most surprising part. The researchers took the broken code the AI wrote and asked the same AI to review it.

• The Result: When asked to review the code, the AI spotted the holes 79% of the time. It knew exactly what was wrong!
• The Problem: But when asked to write the code from scratch, it forgot everything and made the same mistakes again.
• The Analogy: It's like a student who can perfectly grade a test and explain why an answer is wrong, but when they take the test themselves, they get the same questions wrong. They have the knowledge, but they can't apply it while they are working.

The Bottom Line

The paper concludes that AI coding assistants are currently unsafe to use for critical systems without heavy human supervision.

• Don't trust the "Secure" prompt: It doesn't fix the core problem, even when tested on specific subsets of data.
• Don't trust the standard tools: They are blind to the specific math errors AI makes.
• The Solution: We need to treat AI code like it's written by a stranger who doesn't know the rules. We need to use "mathematical proof" (like the Z3 tool) or very careful human experts to check the work before we let it into our digital homes.

In short: The AI is a fast, confident, but dangerously careless apprentice. Until we teach it to build safely from the ground up, we can't just ask it to "be careful."

Technical Summary

1. Problem Statement

The rapid adoption of Large Language Models (LLMs) for generating production code in security-sensitive domains (e.g., web backends, embedded systems, cryptography) has outpaced the understanding of the security properties of their outputs. While prior studies have identified vulnerability patterns in AI-generated code, they rely heavily on static pattern matching or manual inspection. These methods are insufficient because they cannot definitively establish exploitability. A pattern match suggests a potential issue, but it does not prove that a concrete input exists to trigger a fault. Consequently, the true rate of proven vulnerabilities in frontier LLMs remains unquantified, and industry-standard static analysis tools may be failing to detect critical flaws.

2. Methodology

The authors, Dominik Blain and Maxime Noiseux of Cobalt AI, conducted a rigorous empirical study involving 3,500 code artifacts generated by seven frontier LLMs across 500 security-critical prompts.

Experimental Design

• Corpus: 500 natural-language prompts distributed across five Common Weakness Enumeration (CWE) categories:
  • MEM: Buffer allocation and memory management (CWE-131/190).
  • INT: Integer arithmetic and type casting (CWE-190/195).
  • AUTH: Password hashing and session management (CWE-916).
  • CRYPTO: Key generation and random number usage (CWE-327/330).
  • INP: SQL construction and shell command composition (CWE-89/22/78).
• Models Evaluated: GPT-4o, GPT-4.1, Claude Haiku 4.5, Gemini 2.5 Flash, Mistral Large, Llama 3.3 70B, and Llama 4 Scout.
• Configuration: All models were queried at temperature 0 (deterministic mode) via production APIs to ensure reproducibility.

The COBALT Analysis Pipeline

Instead of relying on heuristics, the study employed a formal verification approach:

1. Pattern Extraction: AST-level patterns identify candidate vulnerability sites (e.g., malloc(n * sizeof(T))).
2. Z3 SMT Encoding: Vulnerability conditions are encoded as Satisfiability Modulo Theories (SMT) formulas. For example, integer overflow is checked by verifying the satisfiability of n × sizeof(T) < n under 32-bit unsigned semantics.
3. Witness Extraction: If the Z3 solver returns SAT (satisfiable), a concrete witness value (e.g., a specific integer n that causes overflow) is extracted. This constitutes a mathematical proof of exploitability.
4. Runtime Validation: Selected findings were compiled into Proof-of-Concept (PoC) harnesses and executed with GCC AddressSanitizer (ASAN) to confirm runtime crashes (e.g., heap buffer overflows).

Auxiliary Experiments

• Secure Prompt Ablation: Testing if explicit security instructions in system prompts reduce vulnerability rates. Note: This specific ablation study was conducted on a 50-prompt sub-corpus (v1), distinct from the full 500-prompt benchmark, to assess the efficacy of security instructions under controlled conditions.
• Tool Comparison: Benchmarking the COBALT/Z3 detection rate against six industry-standard tools (Semgrep, Bandit, Cppcheck, Clang Static Analyzer, FlawFinder, CodeQL).
• Generation-Review Asymmetry: Testing if models can identify vulnerabilities in their own code when asked to review it, compared to when they generate it.

3. Key Contributions

1. Formal Verification at Scale: This is the first study to apply Z3 SMT solving to 3,500 AI-generated artifacts to establish ground-truth exploitability rather than just potential risk.
2. Quantification of the "Broken by Default" State: The study provides concrete statistics showing that current frontier models produce insecure code by default, with no model achieving a security grade better than "D."
3. Structural Gap Identification: The research demonstrates that existing industry tools (including heavyweight semantic analyzers like CodeQL) miss 97.8% of formally proven vulnerabilities because they lack the arithmetic reasoning capabilities to detect integer overflows in allocation logic.
4. Generation-Review Asymmetry: The study reveals that models possess the knowledge to detect these vulnerabilities (78.7% detection rate in review mode) but fail to apply this knowledge during generation (55.8% vulnerability rate), indicating a failure in the generation prior rather than a lack of security knowledge.

4. Key Results

Vulnerability Rates

• Mean Vulnerability Rate: 55.8% of all generated artifacts contained at least one COBALT-identified vulnerability.
• Formally Proven (Z3 SAT): 1,055 findings were mathematically proven to be exploitable.
• Model Performance:
  • Worst: GPT-4o (62.4% vulnerability rate, Grade F).
  • Best: Gemini 2.5 Flash (48.4% vulnerability rate, Grade D).
  • Critical Finding: No model achieved a Grade C or better.
• Category Breakdown:
  • Integer Arithmetic (INT): 87% vulnerability rate (highest).
  • Memory Allocation (MEM): 67% vulnerability rate.
  • Input Handling (INP): 56%.
  • Authentication (AUTH): 44%.
  • Cryptography (CRYPTO): 25%.

Runtime Validation

• 6 out of 7 selected PoCs resulted in confirmed runtime crashes (e.g., heap buffer overflows, SQL injection data exfiltration) when executed with AddressSanitizer.
• One case (Zip Slip) was blocked by Python 3.12 runtime checks, but the vulnerable pattern was still present.

Auxiliary Findings

• Secure Prompts are Ineffective: Adding explicit security instructions reduced the mean vulnerability rate by only 4 percentage points (from 64.8% to 60.8%) in the 50-prompt sub-corpus (v1) ablation study. Four of five models remained at Grade F.
• Tool Failure:
  • Six industry tools combined flagged only 7.6% of artifacts.
  • They missed 97.8% of the Z3-proven vulnerabilities.
  • CodeQL (v2.25.1) detected 0 out of 90 formally proven findings (100% miss rate).
  • Reason: Tools rely on pattern matching or taint tracking, which cannot prove that malloc(n * sizeof(T)) is unsafe without concrete arithmetic reasoning across the full domain of integer inputs.
• Generation-Review Asymmetry: Models correctly identified their own Z3-proven vulnerabilities 78.7% of the time in review mode, yet generated them 55.8% of the time by default.

5. Significance and Implications

The paper concludes that AI coding assistants are "broken by default" regarding security. The findings challenge the assumption that "secure prompting" or standard static analysis is sufficient for AI-generated code.

• Methodological Shift: The study argues that Formal Verification (Z3 SMT) is the only methodology capable of establishing ground-truth exploitability for the specific class of vulnerabilities (integer overflows in allocation arithmetic) that dominate AI-generated code.
• Developer Guidance:
  • Treat all AI-generated C/C++ code as unreviewed and requiring explicit security audits.
  • Do not rely on security prompt prefixes as a mitigation.
  • Do not rely on current industry tools (Semgrep, CodeQL, etc.) to catch AI-generated integer overflows.
  • Use formal verification or rigorous human review for allocation arithmetic.
• Future Work: The authors call for mandatory formal verification in AI code review pipelines and suggest that future model training must address the "generation prior" bias toward insecure patterns found in training data.

Reproducibility: The full dataset of 3,500 artifacts with Z3 labels, prompts, and analysis scripts are publicly available at https://github.com/dom-omg/broken-by-default.