Verified Drone Altitude Control — A Formal Methods Approach

01 // Abstract

The Core “Why”

Genesis

I realized that unit testing isn’t enough for drones where a single software bug equals a total loss. I wanted to treat the control law not as code, but as a mathematical theorem.

Learning Curve

I spent weeks diving into the RTCA DO-178C standard and learning the SMT-LIB language to understand how Z3 (Microsoft Research) actually “thinks” about real numbers.

Struggle

My biggest challenge was bridging the gap between abstract math and real-time physics. I had to build a custom GCS (Ground Control Station) in Pygame just to see the “verified” flag in action.

Breakthrough

Using Manim to visualize the counter-examples Z3 found was the “aha!” moment. It showed me exactly where the logic was weak before a single line of flight code was run.

02 // The Invariants

Safety Constraints — Formally Discharged

; Admissible input domain (SMT-LIB 2.0)
(declare-const alt_m      Real)
(declare-const obs_dist_m Real)
(declare-const v_spd_mps  Real)

(assert (and (>= alt_m      0.0)   (<= alt_m      200.0)))
(assert (and (>= obs_dist_m 0.0)   (<= obs_dist_m 200.0)))
(assert (and (>= v_spd_mps -10.0)  (<= v_spd_mps  10.0)))

INV-001

compute_target_alt(…) ≥ MIN_ALT_M (2.0 m)

Z3 tactic: assert output < 2.0 → unsat → PROVED

INV-002

compute_target_alt(…) ≤ MAX_ALT_M (120.0 m)

Z3 tactic: assert output > 120.0 → unsat → PROVED

INV-003

Avoidance climbs bounded within [2.0, 120.0] m

Z3 tactic: assert climb AND envelope violation → unsat → PROVED

# Verification output — Z3 4.16.0

  [PROVED]  INV-001   compute_target_alt() >= 2.0 m     0.92 ms
  [PROVED]  INV-002   compute_target_alt() <= 120.0 m   0.43 ms
  [PROVED]  INV-003   Avoidance climb bounded            0.86 ms

  VERDICT : ALL INVARIANTS PROVED

03 // Hardened Architecture

The “No Exceptions” Rule

In safety-critical systems, exceptions are an unstructured control flow mechanism that cannot be statically reasoned about. Every function in this project returns an explicit, typed result object whose state transitions are fully enumerable at compile time.

No try/except

All outcomes are explicit VerificationStatus enum values. Callers must branch on status before accessing payload fields. This mirrors the Result<T, E> idiom in Rust and Ada’s explicit return status pattern.

Unit Suffixes

All physical quantities carry unit suffixes: _m (meters), _mps (meters per second), _s (seconds). No naked floats.

typing.Final

All safety constants are declared with typing.Final. Domain types use NewType for Meters and MetersPerSecond to prevent dimensional errors.

Linear Arithmetic

The Z3 symbolic model uses only linear real arithmetic — decidable by the LA(Q) tactic without requiring nonlinear extensions. This guarantees solver termination.

# Architecture map

drone_logic.py          Control law (plant model under verification)
verify_z3.py            SMT assertions, counterexample extraction
result_types.py         Typed result objects (no exceptions used)
simulate.py             Physics trajectory generator
gcs_pygame.py           Amber-on-black GCS display (Pygame)
manim_counterexample.py 3-act counterexample animation (Manim)
visualize.py            Matplotlib animation (fallback)
main.py                 Pipeline entry point with --mode selector

04 // Verification vs Simulation

Proof, Not Evidence

Unit tests provide inductive evidence. Z3 provides a deductive proof. For compute_target_alt, the property MIN_ALT_M ≤ output ≤ MAX_ALT_M is now a theorem, not a conjecture.

Criterion	Unit Tests	Z3 Formal Verification
Input coverage	Finite, hand-picked samples	Complete continuous domain
Bug discovery	Only tested cases	Any input — no gaps
Guarantee	Evidence	Mathematical proof
Counterexample	None	Exact violating assignment
Standard	Universal	NASA FM, DO-333, AWS IAM

# Counterexample demonstration (unsafe variant, clamp removed)

  [FALSIFIED]  INV-002-UNSAFE
               Counterexample:
                 alt_m      = 121.111111 m
                 obs_dist_m =  15.000000 m
                 v_spd_mps  =   0.555556 m/s
                 output_m   = 120.555556 m  [violates [2.0, 120.0] m]

  VERDICT : 1 INVARIANT(S) FALSIFIED — DO NOT DEPLOY

05 // Media

Showcase

Ground Control Station — Pygame GCS Display [SMT-VERIFIED]

Simulation GIF — Drone altitude control simulation in action

Simulation — Altitude Control Loop

Manim Counterexample Animation — 3-Act Visualization