# All Artificial, Less Intelligence: GenAI through the Lens of Formal Verification

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

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 22 references that are in the map.
- First posted on arXiv 25 Mar 2024.

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

- [CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis](https://mlsanity.com/paper/2203.13474/) (2022)
- [RTLLM: An Open-Source Benchmark for Design RTL Generation with Large Language Model](https://mlsanity.com/paper/2308.05345/) (2023)
- [Chip-Chat: Challenges and Opportunities in Conversational Hardware Design](https://mlsanity.com/paper/2305.13243/) (2023)
- [Benchmarking Large Language Models for Automated Verilog RTL Code Generation](https://mlsanity.com/paper/2212.11140/) (2022)
- [ChipGPT: How far are we from natural language hardware design](https://mlsanity.com/paper/2305.14019/) (2023)
- [The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification](https://mlsanity.com/paper/2307.02192/) (2023)

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

- [LLMs in Web Development: Evaluating LLM-Generated PHP Code Unveiling Vulnerabilities and Limitations](https://mlsanity.com/paper/2404.14459/) (2024)
- [Saarthi: The First AI Formal Verification Engineer](https://mlsanity.com/paper/2502.16662/) (2025)
- [Generative AI Augmented Induction-based Formal Verification](https://mlsanity.com/paper/2407.18965/) (2024)
- [A Multi-Agent Generative AI Framework for IC Module-Level Verification Automation](https://mlsanity.com/paper/2507.21694/) (2025)
- [CODMAS: A Dialectic Multi-Agent Collaborative Framework for Structured RTL Optimization](https://mlsanity.com/paper/2603.17204/) (2026)
- [VeriCWEty: Embedding enabled Line-Level CWE Detection in Verilog](https://mlsanity.com/paper/2604.15375/) (2026)
- [ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols](https://mlsanity.com/paper/2506.07945/) (2025)
- [Towards Automated Formal Verification of Backend Systems with LLMs](https://mlsanity.com/paper/2506.10998/) (2025)
- [Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification](https://mlsanity.com/paper/2603.03175/) (2026)
- [SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation](https://mlsanity.com/paper/2605.25181/) (2026)
- [Evaluating Generative AI-Enhanced Content: A Conceptual Framework Using Qualitative, Quantitative, and Mixed-Methods Approaches](https://mlsanity.com/paper/2411.17943/) (2024)

## Abstract (arXiv)

Modern hardware designs have grown increasingly efficient and complex. However, they are often susceptible to Common Weakness Enumerations (CWEs). This paper is focused on the formal verification of CWEs in a dataset of hardware designs written in SystemVerilog from Regenerative Artificial Intelligence (AI) powered by Large Language Models (LLMs). We applied formal verification to categorize each hardware design as vulnerable or CWE-free. This dataset was generated by 4 different LLMs and features a unique set of designs for each of the 10 CWEs we target in our paper. We have associated the identified vulnerabilities with CWE numbers for a dataset of 60,000 generated SystemVerilog Register Transfer Level (RTL) code. It was also found that most LLMs are not aware of any hardware CWEs; hence they are usually not considered when generating the hardware code. Our study reveals that approximately 60% of the hardware designs generated by LLMs are prone to CWEs, posing potential safety and security risks. The dataset could be ideal for training LLMs and Machine Learning (ML) algorithms to abstain from generating CWE-prone hardware designs.