LLM-Guided Security Claim Generation for Autonomous Vehicle in Smart Urban Systems

This paper presents a novel evaluation framework that uses Large Language Models (LLMs) to automatically generate formal security assertions for autonomous vehicle (AV) subsystems an area that remains insufficiently explored in the context of hardware-level safety verification. While LLMs have demonstrated capabilities in tasks such as perception, route planning, and user interaction, their role in generating formal assertions for low-level AV hardware components has not been systematically studied. The proposed framework addresses this gap by guiding LLMs to generate SystemVerilog Assertions (SVAs) across four AV-related benchmarks, each corresponding to a distinct hardware vulnerability classified by Common Weakness Enumerations (CWEs). These benchmarks include traffic signal controllers, AES encryption modules, privilege-level register controllers, and ADC reset logic. The framework incorporates structured prompt engineering, syntax correction, and simulation-based validation to assess the correctness of generated assertions. Experimental results using OpenAI’s Codex show that LLMs can produce correct assertions in more than 50% of cases when complete design context is provided, while performance drops significantly with minimal input. This study introduces the first comprehensive benchmark and evaluation pipeline for LLM-generated SVAs in AV systems and offers new insights into the potential of generative models to support formal verification in intelligent transportation and smart city infrastructures.