AdaCore has outlined how Ada and the SPARK programming language subset can be integrated with the Zephyr RTOS through the Alire skill.
The approach connects Ada’s GNAT Project and gprbuild environment with Zephyr’s CMake, west, and device tree infrastructure, reducing the manual work traditionally required to align toolchains, integrate build systems, and create interoperability layers between Ada and C. Enabling Ada and SPARK on top of Zephyr allows developers to use a wide range of Zephyr-supported embedded boards from vendors including NXP, STMicroelectronics, and Analog Devices.
The workflow is demonstrated through Open-Sesame, an in-development garage door controller running on an STMicroelectronics NUCLEO-H563ZI board. In this architecture, Ada and SPARK manage the MQTT state machine, door logic, and provisioning functions, while Zephyr provides the scheduler, drivers, network stack, and board support package. A thin C hardware abstraction layer connects the Ada application layer to Zephyr’s APIs, allowing interoperability between the two environments while preserving compatibility with Zephyr’s macro-based systems.
The article also details how the Alire skill manages cross-compilation dependencies, configures build environments, integrates gprbuild into the CMake workflow, and supports GNATprove verification processes. Additional topics include static library generation, linker configuration, floating-point ABI alignment, Ada and C interoperability patterns, and portability across multiple hardware targets.
