Symbolic and Safety-Centric Formal Verification of MAVLink for Autonomous eVTOL Systems

The growing use of autonomous electric Vertical Takeoff and Landing (A-eVTOL) vehicles demands secure and reliable command and control (C2) communication to meet stringent safety and regulatory requirements. MAVLink (Micro Air Vehicle Link), a lightweight protocol widely adopted in UAV systems, lacks standardized encryption and authentication mechanisms, exposing it to critical threats such as spoofing and message tampering. This paper presents a formal verification framework that models MAVLink’s behavior in the context of A-eVTOL operations. We identify how its vulnerabilities, tolerable in traditional UAV use, are amplified under eVTOL specific constraints such as real-time responsiveness, autonomy, and fail-safe guarantees. To the best of our knowledge, this is the first work to formally analyze MAVLink in a safety critical eVTOL setting, revealing attack paths and proposing formally guided cryptographic mitigation strategies tailored to autonomous flight. Our findings offer new insights for certifying lightweight protocols in next generation aerial mobility systems.