As 5G and NextG systems grow in complexity, ensuring security and correctness requires verification approaches that are both scalable and trustworthy. This talk highlights recent progress from the MACC Lab at Stevens Institute of Technology, developed with DARPA, including our new system Auto-modeling of Formal Verification with Real-world Prompting (AVRE). AVRE leverages large language models (LLMs) to transform protocol descriptions into dependency graphs and formal models, using cross- and self-attention with transformer-based reasoning to resolve ambiguities, capture design intent, and establish quantifiable dependencies. Integrated with our HyFuzz hybrid fuzzing platform, AVRE closes the loop between formal modeling and experimental validation. Together, these advances demonstrate a robust, AI-assisted pipeline for formal verification and vulnerability detection in cyber-physical and wireless systems, paving the way for practical assurance frameworks in contested and mission-critical environments. Co-sponsored by: Fairleigh Dickinson University Speaker(s): Ying Wang Agenda: Fairleigh Dickinson University 1000 River Road, Building: Muscarelle Center, Room Number: 105 Teaneck, New Jersey, United States 07666 For additional information about the venue and parking, please contact Dr. Hong Zhao zhao@fdu.edu Bldg: M105, 1000 River Road, Teaneck, New Jersey, United States, 07666