certiflie
GPL-3.0Ada
Ada and SPARK firmware for the Crazyflie 2.0 nano quadcopter, targeting the STM32F4 ARM chip.
35 stars18 forks0 contributors
Overview
This project provides a complete firmware implementation for the Crazyflie 2.0 drone, written in Ada 2012 and SPARK 2014. It demonstrates the use of high-assurance programming languages for embedded systems on an ARM-based STM32F4 microcontroller.
Key Features
- Ada + SPARK Implementation — Uses Ada 2012 for the main codebase and SPARK 2014 for formal verification, targeting embedded safety and reliability.
- Ravenscar-Full Runtime — Employs a high-integrity runtime system designed for real-time, concurrent applications on the STM32F4.
- STM32F4 DFU Flashing — Supports deployment via Device Firmware Update mode using standard tools like dfu-util.
- Git Submodule Integration — Manages dependencies, including the Ada_Drivers_Library, through recursive git submodules.
Philosophy
The firmware emphasizes reliability and formal verification through the use of Ada and SPARK, aiming to provide a robust, high-assurance codebase for embedded drone control.
Community-curated · Updated weekly · 100% open source
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.