Abstract
Certifying an autonomous drone for operation beyond visual line of sight (BVLOS) requires demonstrating not just that the vehicle usually behaves safely, but that it cannot violate specified safety properties under any reachable state. Formal verification, which provides mathematical guarantees rather than empirical evidence, is entering drone system design through two practical routes: reachability analysis for flight envelope protection and runtime monitoring using synthesized invariant monitors. Neither approach covers the full autonomy stack yet, but both are now appearing in pre-certification packages submitted to the FAA and EASA.
Reachability Analysis for Flight Envelope Protection
Reachability analysis computes the set of states a dynamical system can occupy over a time horizon from a given initial set, given worst-case disturbances. For a quadrotor or fixed-wing UAV, the safety property is typically that the state trajectory stays inside a defined flight envelope - bounded altitude, airspeed, roll, and proximity to restricted airspace. Tools such as Flow*, DryVR, and the MATLAB Aerospace Toolbox’s reachability extensions have been applied to linearized and nonlinear UAV models. The challenge is scalability: high-fidelity aerodynamic models with dozens of state variables produce reachability problems that current solvers cannot close in reasonable time. Most verified envelopes use simplified dynamics with explicit conservatism bounds, meaning the verified envelope is smaller than the true flyable region.
Neural Network Controller Verification
Modern drone autopilots increasingly incorporate neural network components, particularly for state estimation and trajectory tracking under sensor noise. Verifying properties of neural controllers requires tools beyond classical reachability analysis. Satisfiability modulo theories solvers adapted for piecewise-linear networks (Marabou, alpha-beta CROWN) and abstract interpretation frameworks (AI2, ERAN) can verify local input-output properties of small networks but have not yet scaled to the sizes used in production flight controllers. Research groups at Stanford’s AeroCASE lab and at TU Munich have published compositional approaches where the neural component is verified modularly against a specification, and the specification is separately verified against the system safety property, reducing the monolithic verification burden.
Runtime Monitoring as a Complement
Where full offline verification is intractable, runtime monitors synthesized from temporal logic specifications provide a complementary safety layer. A monitor observes the vehicle state at each control cycle and raises a flag if any safety invariant is about to be violated, triggering a pre-verified failsafe maneuver. Synthesizing monitors from Signal Temporal Logic (STL) or Metric Temporal Logic (MTL) specifications is well-understood for linear systems. The harder problem is monitor latency: a monitor that detects a violation 200ms too late may find the vehicle already outside the recoverable envelope. DARPA’s Assured Autonomy program funded work on predictive monitors that flag invariant violations before they occur, using short-horizon reachable sets computed online.
Certification Pathway
EASA’s Easy Access Rules for BVLOS operations and the FAA’s forthcoming UAS-specific means of compliance both acknowledge formal methods as an acceptable verification technique, but neither specifies required coverage levels or tool qualification standards. Industry working groups, including the EUROCAE WG-105 and the RTCA SC-228 subcommittees, are drafting guidance that would allow formal verification artifacts to substitute for some flight test hours. Until those standards finalize, the practical certification value of formal verification is most in reducing the number of required flight test scenarios by establishing bounded coverage of a well-defined state space.