Ada on Zephyr: How the Alire Skill Wires It Together

Ada is a programming language popular for high-integrity software, especially its SPARK subset, which provides static, compile-time proof of the absence of runtime errors. Zephyr is an open source real-time operating system with broad support across many embedded boards from vendors such as NXP, STMicroelectronics, Analog Devices, and more.

Enabling Ada and SPARK on top of Zephyr lets makers choose from a wide array of boards to build their systems.

The two ecosystems that did not grow up together: Ada, with its GNAT Project files and gprbuild, and Zephyr, with CMake, west, and a device tree. Both are excellent at what they do. Neither knows the other exists.

Getting Ada to run on Zephyr was never difficult, just laborious. It requires shim layers of the C code that the Ada layer depends on, integrating the build systems, finding compilers, aligning them, and iterating till everything works. There is a fantastic video by J German Rivera that goes into the details here.

LLMs can make this process easier, but they will need to determine which steps are required for each board and program. A SKILL is a way to teach an LLM about a specific topic. The Alire skill published by AdaCore at https://github.com/AdaCore/skills/alire distills the necessary knowledge and presents it to the LLM.

This makes integrating Ada code into Zephyr as simple as a single LLM prompt and a single make command. ‘Can you create a new project, call it <project name> and implement the dining philosophers on Zephyr on the <board> board using the /alire skill?’ Just fill in your project name and the Zephyr-supported board, and off you go.

This post is about what happens between make and a flashed binary, because anyone shipping safety-critical firmware should understand the machinery they depend on.

The reference project is Open-Sesame, an in-development garage door controller running on a NUCLEO-H563ZI. Ada and SPARK handle the MQTT state machine, door logic, and provisioning. Zephyr handles everything from the scheduler down. They meet at a thin C shim layer.

The Three-Tier Architecture

┌─────────────────────────────────────────────┐
│        Ada / SPARK application              │
│   business logic, formally verified         │
├─────────────────────────────────────────────┤
│        C HAL shim                           │
│   wraps Zephyr's macro-heavy APIs           │
├─────────────────────────────────────────────┤
│        Zephyr RTOS                          │
│   scheduler, drivers, network stack, BSP    │
└─────────────────────────────────────────────┘

Ada owns the code that benefits from formal reasoning. Zephyr owns the code that benefits from a battle-tested C ecosystem. The C shim exists because Zephyr's GPIO, device tree, and Kconfig systems lean heavily on preprocessor macros, GPIO_DT_SPEC_GET expands to a struct initializer referencing generated symbols, and you cannot call a macro from Ada. A function call wrapper is the correct fix, not a compromise.

What Alire Does Before The Build Starts

Ada cross-compilation needs three tools on PATH at the right moment: arm-eabi-gcc, gprbuild, and (for proof) gnatprove. Historically, each developer installed these by hand, then maintained shell scripts to ensure CMake recognized them. The skill replaces that with a declaration in alire.toml

toml

[[depends-on]]
gnat_arm_elf = "any"      # arm-eabi-gcc cross compiler
gprbuild     = "any"      # builds the Ada static library
gnatprove    = "^15.1.0"  # SPARK proof, runs natively

On the first invocation of alr exec, Alire resolves these as crates, pulls them into a per-project cache, and injects PATH, GPR_TOOL_PREFIX, and the rest of the environment before running the actual command. There is no alr toolchain --select step, no global install, no version skew between developers. A new hire clones the repo and runs make. The first build is slow because Alire is downloading; subsequent builds are fast.

How CMake Discovers gprbuild

Once Alire has populated PATH, the CMakeLists.txt does the rest. Four operations matter.

First, it locates the Ada toolchain by asking PATH:

cmake

find_program(ADA_COMPILER arm-eabi-gcc REQUIRED)
find_program(ADA_GPRBUILD gprbuild     REQUIRED)
get_filename_component(ADA_BIN_DIR       "${ADA_COMPILER}" DIRECTORY)
get_filename_component(ADA_TOOLCHAIN_DIR "${ADA_BIN_DIR}"  DIRECTORY)

Because the Makefile launches the build with alr exec -- west build ..., PATH is already correct. CMake just reads it.

Second, it parses the runtime name out of the GPR file rather than duplicating it:

cmake

file(READ "${CMAKE_CURRENT_SOURCE_DIR}/open_sesame_cross.gpr" _gpr_content)
string(REGEX MATCH "for Runtime \\(\"Ada\"\\) use \"([^\"]+)\"" _ "${_gpr_content}")
set(ADA_RTS "${CMAKE_MATCH_1}")

The GPR file is the GNAT compiler's multi-language build environment. It contains the information about which Ada runtime to use, currently light-cortex-m33f, the lightweight bare-metal runtime for Cortex-M33 with hard-float ABI. CMake reads it instead of carrying its own copy, which prevents the two from drifting apart.

Third, it locates libgnat.a early, so a misconfigured toolchain fails loudly at configure time rather than producing a corrupt binary at link time:

cmake

find_file(ADA_LIBGNAT "libgnat.a"
  PATHS "${ADA_TOOLCHAIN_DIR}/${ADA_TARGET}/lib/gnat/${ADA_RTS}/adalib"
  NO_DEFAULT_PATH REQUIRED)

Fourth, it runs gprbuild as a custom command, captures libada_app.a, and adds it to the Zephyr link line:

cmake

add_custom_command(
  OUTPUT "${ADA_LIB}"
  COMMAND ${CMAKE_COMMAND} -E env
    "PATH=${ADA_BIN_DIR}${_path_sep}$ENV{PATH}"
    "GPR_TOOL_PREFIX=${ADA_TOOL_PREFIX}"
    "${ADA_GPRBUILD}"
      -P "${ADA_CROSS_GPR}"
      -j0
      --target=${ADA_TARGET}
      -XADA_OBJ_DIR="${ADA_OBJ_DIR}"
  DEPENDS ${ADA_SOURCES} "${ADA_CROSS_GPR}"
)
add_custom_target(ada_lib ALL DEPENDS "${ADA_LIB}")
add_dependencies(app ada_lib)
target_link_libraries(app PRIVATE "${ADA_LIB}" "${ADA_LIBGNAT}")
zephyr_ld_options("-Wl,--allow-multiple-definition")

The Ada side compiles to a static library because that is the simplest possible artifact for CMake to link, no .so, no dlopen dance, just an archive of object files.

The Cross-Compilation GPR

The GPR file describes how Ada should be compiled for the target:

ada

project Open_Sesame_Cross is
   for Target use "arm-eabi";
   for Runtime ("Ada") use "light-cortex-m33f";

   for Library_Name use "ada_app";
   for Library_Kind use "static";

   package Compiler is
      for Default_Switches ("Ada") use
        ("-mcpu=cortex-m33", "-mthumb",
         "-mfpu=fpv5-sp-d16", "-mfloat-abi=hard",
         "-Os", "-g", "-gnat2022", "-gnatwa");
   end Compiler;
end Open_Sesame_Cross;

Three lines carry weight. light-cortex-m33f is the runtime, no tasking, no secondary stack, minimal elaboration overhead, which is what you want when Zephyr is already providing the scheduler. -mfloat-abi=hard must match Zephyr's CONFIG_FPU=y, or float arguments are passed in different registers on each side and corruption follows. Library_Kind => "static" produces libada_app.a.

Two Linker Gotchas Worth Knowing

The skill papers over two real problems, both worth understanding.

abort() is defined twice. libgnat.a ships with one definition, Zephyr's libc ships with another. Without intervention, the linker errors out. The fix:

cmake 

zephyr_ld_options("-Wl,--allow-multiple-definition")

This tells the linker to take the first definition it sees and move on. Because Zephyr's libc appears earlier in the link line, Zephyr's abort() wins, and it is the correct one, since it integrates with the kernel's fatal error handler. Ada's abort() is unreachable, which is fine.

Float ABI must match. If Ada is compiled with -mfloat-abi=hard and Zephyr with soft-float, or vice versa, the code links cleanly and crashes mysteriously at runtime. Both sides must agree. The skill enforces hard-float on the Ada side via the GPR; you must ensure CONFIG_FPU=y on the Zephyr side.

How Ada and C Talk

Three patterns cover essentially every interaction.

Ada calling C. Write a thin C function, import it on the Ada side. By convention, every C function exposed to Ada starts with ada_, so it is obvious at the call site that you are crossing a language boundary:

ada

procedure C_Pulse_Relay
  with Import, Convention => C, External_Name => "ada_hal_pulse_relay";

C calling Ada. Export an Ada procedure. Zephyr's MQTT callback fires from C, calls into Ada, and Ada's dispatcher takes over:

ada

procedure Ada_Dispatch_Command (Payload : chars_ptr)
  with Export, Convention => C,
       External_Name => "ada_dispatch_command";

Verified spec, trusted body. This is the pattern that makes formal verification practical in the presence of C interop. SPARK cannot reason about Import and Export pragmas, they bypass the information flow model. So put pragma SPARK_Mode (On) on the spec, where contracts live, and pragma SPARK_Mode (Off) on the body, where the C bindings live:

ada

-- garage_door-hal.ads  (provable)
pragma SPARK_Mode (On);
package Garage_Door.HAL is
   procedure Pulse_Relay with Global => null;
   function Read_Door_Sensor return Boolean
     with Volatile_Function, Global => null;
end Garage_Door.HAL;

-- garage_door-hal.adb  (trusted)
pragma SPARK_Mode (Off);
package body Garage_Door.HAL is
   procedure C_Pulse_Relay
     with Import, Convention => C, External_Name => "ada_hal_pulse_relay";
   ...
end Garage_Door.HAL;

GNATprove verifies every caller against the contract. The body is reviewed and tested like normal C code. Most safety-critical bugs live in business logic, not in a one-line GPIO toggle, so this trade-off lands where it should.

Portability for Free

A side benefit of the shim layer: targeting a new board means rewriting C, not Ada. The same Open-Sesame project runs on a Raspberry Pi Pico W (WiFi) and an STM32H563ZI (Ethernet). The Ada Garage_Door.Wifi.Connect procedure has the same signature on both. The implementation lives in different C files:

c

/* wifi_zephyr.c */
int ada_wifi_connect(const char *ssid, const char *psk) {
    /* NET_REQUEST_WIFI_CONNECT, wait on semaphore */
    return k_sem_take(&wifi_sem, K_SECONDS(30)) ? -ETIMEDOUT : 0;
}

/* eth_zephyr.c */
int ada_wifi_connect(const char *ssid, const char *psk) {
    (void)ssid; (void)psk;
    net_dhcpv4_start(iface);
    return k_sem_take(&ipv4_sem, K_SECONDS(30)) ? -ETIMEDOUT : 0;
}

CMake selects the right shim based on the board target. The Ada code does not change.

Proof Runs On The Host

The cross-compilation GPR is used to build firmware. A separate, host-only GPR drives proof:

ada

project Open_Sesame is
   for Source_Dirs use ("src");
   package Prove is
      for Proof_Switches ("Ada") use
        ("--level=1", "-j0", "--warnings=continue",
         "--output=oneline", "--report=all");
   end Prove;
end Open_Sesame;

bash

alr exec -- gnatprove -P open_sesame.gpr

GNATprove runs natively on your laptop or CI runner, no cross-compilation involved. The pattern of SPARK_Mode (On) on specs and SPARK_Mode (Off) on C-interop bodies means contracts are always provable, even when implementations are not. You get the static guarantees where they matter and pay nothing for them where they cannot apply.

The Full Loop

bash

git clone <repo> && cd Open-Sesame
west init -l . && west update     # pull pinned Zephyr
make                              # alr exec -- west build ...
make flash

On first run, alr exec resolves the Ada crates, downloads the cross toolchain, and caches it. CMake finds the toolchain on PATH, reads the GPR file, runs gprbuild, and links the result into the Zephyr image. west flashes the binary. The NUCLEO board boots, opens a UART provisioning terminal at 115200, asks for an MQTT broker, saves it to NVS, reboots into normal operation, and starts publishing.

This does require that Zephyr is installed and that West and the West SDK are installed.

What This Buys You

The pattern here is not groundbreaking. Static libraries, custom CMake commands, foreign function imports, these are all standard tools. What the skill does is encode the correct combination so you, nor the LLM, have to discover it anew every time.

Clone Open-Sesame, run make, and read the CMakeLists.txt while the toolchain downloads. The scaffolding transfers directly to any Ada-on-Zephyr project you want to build next.