Quadcopter Flight Controller

A mixed-criticality flight controller for the Raspberry Pi Pico 2 (RP2350), combining MicroPython for high-level orchestration with SPARK Ada for formally verified flight control.

Architecture

graph TB
    subgraph Core0["Core 0: MicroPython (Untrusted, Dynamic)"]
        AsyncIO["asyncio Control Loop<br/>(500 Hz Tick Caller)"]
        Telem["Telemetry & Logging<br/>(10 Hz Web/Serial)"]
    end

    subgraph Boundary["C Glue Layer"]
        PyModule["flight_module.c<br/>(MicroPython C Binding)"]
    end

    subgraph Core1["Core 1: SPARK Ada (Formally Verified Engine)"]
        AdaBoundary["micropython_flight.adb<br/>(Ada FFI Entry)"]
        FlightCtrl["flight_controller.adb<br/>(Flight Controller Orchestrator)"]

        subgraph Estimator["State Estimation"]
            Attitude["attitude.adb<br/>(Complementary Filter)"]
        end

        subgraph VerifiedCore["Formally Verified Core (SPARK_Mode On)"]
            PID["pid_controller.adb<br/>(PID Controllers - Roll, Pitch, Yaw)"]
            Mixer["motor_mixer.adb<br/>(X-Config Motor Matrix)"]
        end

        subgraph HWBindings["Hardware FFI Bindings"]
            IMUBinding["imu_binding.adb"]
            MotorBinding["motor_binding.adb"]
        end
    end

    subgraph Drivers["C Driver Libraries"]
        IMUBridge["imu_c_bridge.c"]
        MotorBridge["motor_c_bridge.c"]
        MPU6050["lf-mpu6050 (I2C 0x68)"]
        QMC5883L["lf-qmc5883l (I2C 0x0D)"]
        PWM["PWM Motor Control (ESC)"]
    end

    AsyncIO -->|flight.tick| PyModule
    Telem -.->|flight.get_state| PyModule
    PyModule --> AdaBoundary
    AdaBoundary --> FlightCtrl

    FlightCtrl --> IMUBinding
    IMUBinding --> IMUBridge
    IMUBridge --> MPU6050
    IMUBridge --> QMC5883L

    FlightCtrl --> Attitude
    FlightCtrl --> PID
    PID --> Mixer

    Mixer --> MotorBinding
    MotorBinding --> MotorBridge
    MotorBridge --> PWM

    style VerifiedCore fill:#1a3a1a,stroke:#4caf50,stroke-width:2px

What SPARK Proves

The following properties are mathematically guaranteed at compile time via the SPARK prover:

Package	Property	Why It Matters
PID_Controller	Output always in [-1.0, 1.0]	Prevents unbounded integral windup and runaway corrections
Motor_Mixer	All motor values in [0.0, 1.0]	Prevents negative thrust or exceeding motor limits
Flight_Types.Clamp	Result always within [Lo, Hi]	Foundation for all saturation proofs

Run the prover:

cd spark_project
gnatprove -P spark_project.gpr

Project Structure

quadcopter/
├── main.py                          # MicroPython asyncio orchestrator
├── spark_project/
│   └── spark_project.gpr            # GPRBuild project for gnatprove
├── src/
│   ├── micropython.cmake            # Build rules (C + Ada → libflight.a)
│   ├── flight_module.c              # MicroPython C module registration
│   ├── imu_c_bridge.c/h             # C bridge: Ada ↔ lf-mpu6050/lf-qmc5883l
│   ├── motor_c_bridge.c/h           # C bridge: stubbed motor PWM output
│   ├── flight_types.ads/adb         # [SPARK] Shared types and Clamp
│   ├── pid_controller.ads/adb       # [SPARK] PID with saturation contracts
│   ├── motor_mixer.ads/adb          # [SPARK] X-config motor mixing
│   ├── attitude.ads/adb             # [Ada]   Complementary filter
│   ├── flight_controller.ads/adb    # [Ada]   Top-level flight tick
│   ├── imu_binding.ads/adb          # [Ada]   Ada ↔ C IMU bridge
│   ├── motor_binding.ads/adb        # [Ada]   Ada ↔ C motor bridge
│   └── micropython_flight.ads/adb   # [Ada]   Ada ↔ MicroPython boundary
└── tools/
    └── gen_elaboration.sh

Sensor Dependencies

This project links against two sibling Lost + Found driver libraries:

• lf-mpu6050 — MPU6050 6-axis accelerometer/gyroscope (I2C, 0x68)
• lf-qmc5883l — QMC5883L 3-axis magnetometer (I2C, 0x0D)

Both sensors share the I2C0 bus on GP4 (SDA) / GP5 (SCL) at 400 kHz.

Building

cd /path/to/micropython/ports/rp2
make BOARD=RPI_PICO2 USER_C_MODULES=/path/to/quadcopter/src/micropython.cmake

This compiles MicroPython, the C sensor drivers, all Ada/SPARK packages, runs gnatbind for elaboration, and links everything into firmware.elf.

Debugging with GDB

(gdb) break Flight_Controller.Tick
(gdb) break PID_Controller.Compute
(gdb) break Motor_Mixer.Mix

The mixed C/Ada/Python backtrace shows the full call chain from MicroPython bytecode through the C glue into verified Ada.