PAVE-MAVLink: Formal Verification of MAVLink 2 for Secure UAV Communications

This work presents a multi-stage, Large Language Model(LLM)-accelerated framework for formal verification and security validation of UAV communication protocols, focusing on MAVLink 2. We introduce a prompt-driven approach to automatically generate symbolic models for nuXmv and ProVerif, allowing rapid identification and mitigation of protocol vulnerabilities. Experimental results demonstrate that, without cryptographic protections, MAVLink 2 is susceptible to critical command injection attacks, validated through symbolic model checking, software-defined drone simulation, and over-the-air (OTA) testing on physical UAVs. Incorporating ChaCha20 based encryption eliminates these vulnerabilities, as confirmed by formal analysis and empirical validation. These findings illustrate the effectiveness and flexibility of LLM assisted workflows like Prompt Aided Formal Verification (PAVE) while providing a platform for robust cryptographic extensions in advancing UAV protocol security.