  This paper introduces Auto-modeling of Formal Verification with Real-world
Prompting for 5G and NextG protocols (AVRE), a novel system designed for the
formal verification of Next Generation (NextG) communication protocols,
addressing the increasing complexity and scalability challenges in network
protocol design and verification. Utilizing Large Language Models (LLMs), AVRE
transforms protocol descriptions into dependency graphs and formal models,
efficiently resolving ambiguities and capturing design intent. The system
integrates a transformer model with LLMs to autonomously establish quantifiable
dependency relationships through cross- and self-attention mechanisms. Enhanced
by iterative feedback from the HyFuzz experimental platform, AVRE significantly
advances the accuracy and relevance of formal verification in complex
communication protocols, offering a groundbreaking approach to validating
sophisticated communication systems. We compare CAL's performance with
state-of-the-art LLM-based models and traditional time sequence models,
demonstrating its superiority in accuracy and robustness, achieving an accuracy
of 95.94\% and an AUC of 0.98. This NLP-based approach enables, for the first
time, the creation of exploits directly from design documents, making
remarkable progress in scalable system verification and validation.
