Announcing: GNAT Runtime for Ada & SPARK on ESP32
I’m excited to share the latest updates for the espidf_gnat_runtime project!
This runtime allows you to run embedded applications by leveraging the core features and underlying drivers of the ESP-IDF (Espressif IoT Development Framework) on various ESP32 SoCs. By using the proven foundation of the ESP-IDF to support the Ada/SPARK environment, you get the best of both worlds: industry-standard hardware support and the world’s most advanced safety-critical programming language.
Supported SoCs
- RISC-V: ESP32-C3
- Xtensa: ESP32-S3
Key Features
- Concurrency: Support for Ada tasks and protected objects within the requirements of the Jorvik profile, ensuring predictable and efficient multitasking.
- Language Core: Comprehensive support for Exceptions, Controlled types, and Secondary stack for robust memory management and error handling.
- Standard Library: Includes a rich set of the Ada Standard Library:
Ada.Containers(Vectors, Maps, etc.)Ada.Numerics(Elementary functions, Random numbers)Ada.Strings(Fixed, Bounded, and Unbounded)
- Verified Quality: The runtime is rigorously tested with ACATS (Ada Conformity Assessment Test Suite) to ensure language compliance and reliability.
Why Ada & SPARK on ESP32?
By utilizing SPARK, you can move beyond traditional testing to formally prove the correctness of your code and the absence of runtime errors. This makes it an ideal choice for industrial automation, secure gateways, and high-reliability IoT devices where failure is not an option.
Get Started
Ready to build? We’ve provided several ways to jumpstart your development:
- Project Templates: Use our pre-configured templates for both ESP32-C3 and ESP32-S3 to get a working environment in minutes.
- Agent Skill: Use the dedicated agent skill to automate the creation of new projects, handling the boilerplate so you can focus on your logic.