# The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification

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

## Key facts

- Cited by 34 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 73 references that are in the map.
- First posted on arXiv 5 Jul 2023.

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [A Prompt Pattern Catalog to Enhance Prompt Engineering with ChatGPT](https://mlsanity.com/paper/2302.11382/) (2023)
- [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021)
- [The Curse of Recursion: Training on Generated Data Makes Models Forget](https://mlsanity.com/paper/2305.17493/) (2023)
- [Devign: Effective Vulnerability Identification by Learning Comprehensive Program Semantics via Graph Neural Networks](https://mlsanity.com/paper/1909.03496/) (2019)
- [MathPrompter: Mathematical Reasoning using Large Language Models](https://mlsanity.com/paper/2303.05398/) (2023)
- [Do Users Write More Insecure Code with AI Assistants?](https://mlsanity.com/paper/2211.03622/) (2022)
- [Deep Learning based Vulnerability Detection: Are We There Yet?](https://mlsanity.com/paper/2009.07235/) (2020)
- [Towards Accountability for Machine Learning Datasets: Practices from Software Engineering and Infrastructure](https://mlsanity.com/paper/2010.13561/) (2020)
- [Automated Vulnerability Detection in Source Code Using Deep Representation Learning](https://mlsanity.com/paper/1807.04320/) (2018)
- [Examining Zero-Shot Vulnerability Repair with Large Language Models](https://mlsanity.com/paper/2112.02125/) (2021)
- [DiverseVul: A New Vulnerable Source Code Dataset for Deep Learning Based Vulnerability Detection](https://mlsanity.com/paper/2304.00409/) (2023)
- [The Programmer's Assistant: Conversational Interaction with a Large Language Model for Software Development](https://mlsanity.com/paper/2302.07080/) (2023)
- [Lost at C: A User Study on the Security Implications of Large Language Model Code Assistants](https://mlsanity.com/paper/2208.09727/) (2022)
- [How Secure is Code Generated by ChatGPT?](https://mlsanity.com/paper/2304.09655/) (2023)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [CodeTF: One-stop Transformer Library for State-of-the-art Code LLMs](https://mlsanity.com/paper/2306.00029/) (2023)
- [Ensuring Dataset Quality for Machine Learning Certification](https://mlsanity.com/paper/2011.01799/) (2020)
- [SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer](https://mlsanity.com/paper/1810.12041/) (2018)
- [Prompt Sapper: LLM-Empowered Software Engineering Infrastructure for AI-Native Services](https://mlsanity.com/paper/2306.02230/) (2023)

## Built on by (most cited first, 30 of 34)

- [Large Language Models for Software Engineering: A Systematic Literature Review](https://mlsanity.com/paper/2308.10620/) (2023)
- [Purple Llama CyberSecEval: A Secure Coding Benchmark for Language Models](https://mlsanity.com/paper/2312.04724/) (2023)
- [When LLMs Meet Cybersecurity: A Systematic Literature Review](https://mlsanity.com/paper/2405.03644/) (2024)
- [Large Language Models for Cyber Security: A Systematic Literature Review](https://mlsanity.com/paper/2405.04760/) (2024)
- [Constrained Decoding for Secure Code Generation](https://mlsanity.com/paper/2405.00218/) (2024)
- [How secure is AI-generated Code: A Large-Scale Comparison of Large Language Models](https://mlsanity.com/paper/2404.18353/) (2024)
- [LLMs in Web Development: Evaluating LLM-Generated PHP Code Unveiling Vulnerabilities and Limitations](https://mlsanity.com/paper/2404.14459/) (2024)
- [HexaCoder: Secure Code Generation via Oracle-Guided Synthetic Training Data](https://mlsanity.com/paper/2409.06446/) (2024)
- [SecureFalcon: Are We There Yet in Automated Software Vulnerability Detection with LLMs?](https://mlsanity.com/paper/2307.06616/) (2023)
- [All Artificial, Less Intelligence: GenAI through the Lens of Formal Verification](https://mlsanity.com/paper/2403.16750/) (2024)
- [Review of Generative AI Methods in Cybersecurity](https://mlsanity.com/paper/2403.08701/) (2024)
- [Large Language Models for Security Operations Centers: A Comprehensive Survey](https://mlsanity.com/paper/2509.10858/) (2025)
- [ARVO: Atlas of Reproducible Vulnerabilities for Open-Source Software](https://mlsanity.com/paper/2606.17283/) (2026)
- [A Systematic Literature Review on Detecting Software Vulnerabilities with Large Language Models](https://mlsanity.com/paper/2507.22659/) (2025)
- [CompilerDream: Learning a Compiler World Model for General Code Optimization](https://mlsanity.com/paper/2404.16077/) (2024)
- [Helping LLMs Improve Code Generation Using Feedback from Testing and Static Analysis](https://mlsanity.com/paper/2412.14841/) (2024)
- [Dynamic Intelligence Assessment: Benchmarking LLMs on the Road to AGI with a Focus on Model Confidence](https://mlsanity.com/paper/2410.15490/) (2024)
- [Enhancing Source Code Security with LLMs: Demystifying The Challenges and Generating Reliable Repairs](https://mlsanity.com/paper/2409.00571/) (2024)
- [SeCodePLT: A Unified Platform for Evaluating the Security of Code GenAI](https://mlsanity.com/paper/2410.11096/) (2024)
- [Benchmarking AI Models in Software Engineering: A Review, Search Tool, and Unified Approach for Elevating Benchmark Quality](https://mlsanity.com/paper/2503.05860/) (2025)
- [SCGAgent: Recreating the Benefits of Reasoning Models for Secure Code Generation with Agentic Workflows](https://mlsanity.com/paper/2506.07313/) (2025)
- [Exploring the Challenges and Opportunities of AI-assisted Codebase Generation](https://mlsanity.com/paper/2508.07966/) (2025)
- [Assessing the Latent Automated Program Repair Capabilities of Large Language Models using Round-Trip Translation](https://mlsanity.com/paper/2401.07994/) (2024)
- [Generative transformations and patterns in LLM-native approaches for software verification and falsification](https://mlsanity.com/paper/2404.09384/) (2024)
- [ARVO: Atlas of Reproducible Vulnerabilities for Open-Source Software](https://mlsanity.com/paper/2408.02153/) (2024)
- [MultiAIGCD: A Comprehensive dataset for AI Generated Code Detection Covering Multiple Languages, Models,Prompts, and Scenarios](https://mlsanity.com/paper/2507.21693/) (2025)
- [Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach](https://mlsanity.com/paper/2312.17353/) (2023)
- [Evaluating and Improving the Robustness of Security Attack Detectors Generated by LLMs](https://mlsanity.com/paper/2411.18216/) (2024)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)
- [Large Language Models in Cybersecurity: Applications, Vulnerabilities, and Defense Techniques](https://mlsanity.com/paper/2507.13629/) (2025)

## Abstract (arXiv)

This paper presents the FormAI dataset, a large collection of 112, 000 AI-generated compilable and independent C programs with vulnerability classification. We introduce a dynamic zero-shot prompting technique constructed to spawn diverse programs utilizing Large Language Models (LLMs). The dataset is generated by GPT-3.5-turbo and comprises programs with varying levels of complexity. Some programs handle complicated tasks like network management, table games, or encryption, while others deal with simpler tasks like string manipulation. Every program is labeled with the vulnerabilities found within the source code, indicating the type, line number, and vulnerable function name. This is accomplished by employing a formal verification method using the Efficient SMT-based Bounded Model Checker (ESBMC), which uses model checking, abstract interpretation, constraint programming, and satisfiability modulo theories to reason over safety/security properties in programs. This approach definitively detects vulnerabilities and offers a formal model known as a counterexample, thus eliminating the possibility of generating false positive reports. We have associated the identified vulnerabilities with Common Weakness Enumeration (CWE) numbers. We make the source code available for the 112, 000 programs, accompanied by a separate file containing the vulnerabilities detected in each program, making the dataset ideal for training LLMs and machine learning algorithms. Our study unveiled that according to ESBMC, 51.24% of the programs generated by GPT-3.5 contained vulnerabilities, thereby presenting considerable risks to software safety and security.