Bare-Metal Ada on the ESP32-S3 — no FreeRTOS, no ESP-IDF

A from-scratch, almost-entirely-Ada software stack for the dual-core ESP32-S3 (Xtensa LX7). The runtime owns both cores — the context switch, interrupt vectors, clock tick, SMP scheduler and inter-core IPI are all its own, written in Ada and Xtensa assembly. FreeRTOS never runs (its scheduler isn't even linked) and there is no ESP-IDF in the build: every example compiles with Alire GNAT alone and boots through our own minimal 2nd-stage bootloader.

The one exception is the optional Wi-Fi driver (libs/esp32s3_wifi): the radio's lower-MAC and PHY are only shipped by Espressif as binaries, so it links their Wi-Fi/PHY libraries — which are Apache-2.0 and fetched, not committed (tools/fetch-wifi-blobs.sh pins them to exact upstream commits and verifies each by sha256). Everything around them — the OS adapter (which maps the blob's RTOS calls onto our Jorvik tasks, so FreeRTOS still never runs), the WPA2 supplicant, and the whole TCP/IP + TLS stack — is pure Ada.

Hardware validation — full-board retest (2026-06-24)

Every driver and the whole runtime were re-verified on real silicon, on a fully-populated ESP32-S3 board (all external devices except an SD card):

• Device drivers — all working: ES8311 codec + mic (440 Hz play and mic-capture loopback), QMI8658C IMU (≈1 g at rest), SHT41 temp/humidity, PCF85063A RTC, TCA9555 GPIO expander, capacitive touch, ST7789 / ST7789-cube / LCD-i8080 displays, anti-aliased B612 font, a multi-sensor dashboard, TX1812 addressable LEDs, and a NMEA GPS parser.
• Peripheral self-tests — all PASS: SHA/AES crypto, GDMA, I2S / RMT / TWAI / UART loopbacks, PCNT, sigma-delta, LEDC + MCPWM PWM, and the general-purpose timer.
• Runtime / tasking — all working: ZCX exceptions, full dynamic tasking (tasks allocated + freed on the heap, with abort), dual-core SMP, rendezvous, interrupt levels, and the PSRAM allocator.

The freestanding C runtime (memcpy/malloc/…) is now Ada too: an O(1) TLSF allocator and the mem*/libc shims, host-tested and hardware-validated.

It is built in three layers:

1. A native GNAT/Ada runtime in three selectable profiles — light-tasking (Jorvik), embedded (ZCX), and full (complete GNARL tasking) — grown from AdaCore's bb-runtimes with a new esp32s3 board and packaged as a pin-consumable Alire crate (crates/esp32s3_rts).
2. A reusable, hardware-verified peripheral HAL (libs/esp32s3_hal) — 25+ task-safe drivers.
3. A pure-Ada ext2/3/4 filesystem with a JBD2 journal (libs/esp32s3_hal/src/ext4) — mounts real ext4 SD cards (read, write, crash recovery) and is cross-validated against the Linux kernel's own e2fsck. Alongside it, a pure-Ada FAT16 reader (libs/esp32s3_hal/src/fat16) for the volumes a Windows PC has to be able to read and write.

New here? Start with QUICKSTART.md. For the developer tooling and IDE setup see TOOLING.md. For the long-form design write-up (the kernel, the HAL, the filesystem, the conformance work) read the book (book/main.pdf) — its LaTeX source is in the same directory.

Blob-free PSRAM bring-up with a real timing tune

Reinforcing the no-ESP-IDF claim, the 2nd-stage bootloader's external octal-PSRAM bring-up is now entirely from-source, and entirely Ada — all five vendored IDF objects (the mspi_timing/GPIO config and the chip init) were reverse-engineered live over JTAG, replaced first with readable C and then ported to ZFP Ada (boot_psram.adb); the bootloader now has no C at all, only Ada plus its assembly prologue. The bring-up calls only documented ROM functions: mode-register programming and the connectivity probe go through the ROM OPI helper, and the controller config is written from the captured (golden) register state.

The PSRAM din sampling is also genuinely calibrated now. The IDF blob runs its tuning sweep at 20 MHz — where the sampling phase is irrelevant — so it always falls back to a vendor default that actually fails at the 80 MHz operating speed (previously papered over by a hand-coded override). The replacement sweeps the din at the real 80 MHz over a bounded SPI1 transaction (a wrong setting returns garbage instead of stalling the bus) — but it deliberately does not simply centre on that window: the SPI1 eye is wider than, and offset from, the cache's own SPI0 eye. A one-off async-preload cache probe measured the real cache eye, and the tune prefers din mode 1, which sits inside it on every octal board tested, whenever the sweep shows that mode in-window. Validated end-to-end by the example's 1 MB checksum. Full write-up: PSRAM_BRINGUP_RESEARCH.md.

What runs on real silicon

• Dual-core SMP — tasks pinned per core (CPU => 1/CPU => 2), cross-core wake-ups via an inter-core poke, and protected-object entries across cores.
• Cooperative and preemptive priority scheduling; the runtime owns the Xtensa level-5 vector (its tick + IPI) and dispatches level-2/3 device interrupts.
• Interrupt-driven delay until / periodic tasks with exact, stable periods.
• Full Ada tasking on the full profile — rendezvous, protected entries, dynamic/nested tasks, dynamic priorities, task attributes, exception propagation, abort, and Ada.Interrupts handlers (static and dynamic).
• Single-precision FPU state preserved across context switches.
• ACATS 4.2 conformance on hardware — zero port-specific defects on every profile (full: 908 PASS of 1559 applicable, one test per image; see below).
• 25+ peripheral drivers and pure-Ada ext4 + FAT16 filesystems (most drivers ship with a hardware self-test; see Testing status).

Quick start

git clone https://github.com/rowsail/ada_esp32s3.git
cd ada_esp32s3                # or unzip a release archive -- no submodules
./x flash gpio0_blink         # build + flash the pure-Ada GPIO0 blink
./x monitor                   # watch the console

./x is the in-repo dispatcher (./x list, ./x flash <example>, ./x monitor, ./x new <name>, ./x debug …). The first build fetches the Alire toolchains and builds the runtime crate. Full setup, prerequisites, and a guided first run are in QUICKSTART.md.

To scaffold a project outside the repo, source export.sh and run esp32-ada init [<dir>] (defaults to the current folder) — see TOOLING.md.

Runtime profiles

Selected per build with ESP32S3_RTS_PROFILE (default light-tasking):

Profile	Tasking model	What you get
light-tasking	Jorvik (Ravenscar+)	Periodic tasks, protected objects, SMP; no exception propagation (heap-less). The lean default.
embedded	Jorvik + ZCX	Adds full exception propagation with names, controlled-type finalization, and a heap.
full	Complete GNARL	Lifts the Jorvik restrictions: rendezvous, selective accept, dynamic/nested tasks, dynamic priorities, abort, dynamic Ada.Interrupts.

light-tasking and embedded set pragma Profile (Jorvik); full is the unrestricted runtime. See the book's profile chapter and the Limitations chapter for the full-profile edges.

Examples

All 97 examples share the same FreeRTOS-free bare boot (examples/common/bare/); build/flash any with ./x flash <short-name> (the esp32s3_ prefix is optional). Run ./x list for the full set with each one's runtime profile — the tables below are a selection.

Boot

Example	What it is
esp32s3_heartbeat	Single-core heartbeat ([ADA] N at 1 Hz)
esp32s3_psram	A 1 MB static array placed in the external 8 MB PSRAM

Peripheral HAL self-tests (most need no wiring — internal loopback / GPIO sampling)

Example	Driver exercised
esp32s3_gpio0_blink	GPIO straight off the registers
esp32s3_uart_loopback	UART internal TX→RX loopback + RTS/CTS flow control
esp32s3_i2c_loopback	I2C master (START/addressing/NACK/multi-byte write)
esp32s3_i2s_loopback	I2S full-duplex DMA loopback, byte-exact
esp32s3_gdma_copy	GDMA mem-to-mem + RAII Channel handle
esp32s3_mcpwm_pwm / esp32s3_ledc_pwm / esp32s3_sdm_output	PWM / LED-PWM / sigma-delta, GPIO-sampled
esp32s3_rmt_loopback / esp32s3_pcnt_count	RMT pulse loopback / pulse counter
esp32s3_twai_loopback	TWAI (CAN) self-test frame, no transceiver
esp32s3_timer_count	GP timer vs the runtime wall clock + alarm
esp32s3_lcd_i8080	8-bit i80 parallel LCD DMA transfer
esp32s3_adc_read / esp32s3_touch_read	SAR ADC / capacitive touch
esp32s3_tlv2556	TI TLV2556 external 12-bit SPI ADC — reference-independent self-test + channel read (CS on a GPIO the SPI driver drives, shared bus)
esp32s3_rtc_sleep / esp32s3_rtcio_hold	Deep sleep + retained memory / RTC-pad hold
esp32s3_crypto	HW SHA-1/224/256 + AES-128/256 vs FIPS vectors

Storage & filesystem

Example	What it is
esp32s3_sd_spi / esp32s3_sdmmc	SD over SPI / native SDHOST — non-destructive sector round-trip
esp32s3_w25q	W25Q256FV SPI NOR flash — JEDEC ID, 4-byte mode, erase + page-program + read-back (CS on a GPIO the SPI driver drives, shared bus)
esp32s3_wl	Dynamic wear-leveling FTL (Block_Dev.WL) over the SPI NOR flash — format, write/verify across mapping moves, remount and re-verify
esp32s3_ext4_flash	A real ext4 filesystem on the SPI NOR flash — install an embedded image through Ext4 → Block_Dev.WL → W25Q_Source, mount read-write, read + create/commit a file (no-journal direct flush)
esp32s3_ext4_mkfs	Format a blank SPI NOR flash to ext4 on-device with Ext4.Mkfs (no host, no image; optional JBD2 journal), then mount read-write, create files + a subdirectory, remount and read back
esp32s3_ext4	Mount a real ext4/3/2 SD card with the pure-Ada filesystem and read a file

Tasking & runtime profiles

Example	What it is
esp32s3_smp	Cross-core mailbox over a protected-object entry
esp32s3_embedded	embedded profile: tagged dispatch, finalization, named exceptions
esp32s3_full_tasking	full profile: dynamic tasks, master wait, abort
esp32s3_rendezvous	full profile: a server task with entries served by selective accept
esp32s3_full_intr	full profile: pragma Attach_Handler / Ada.Interrupts on HW

Wired networking & protocols (a W5500 Ethernet module on SPI2; the socket API is the chip-neutral GNAT.Sockets facade, so the same code runs over Wi-Fi)

Example	What it is
esp32s3_w5500	The whole Ethernet stack, then a GNAT.Sockets echo server
esp32s3_w5500_dhcp / esp32s3_w5500_dns / esp32s3_w5500_ntp	DHCP with lease maintenance / DNS_Client lookup / SNTP time
esp32s3_w5500_http / esp32s3_w5500_weather	HTTP GET over GNAT.Sockets / a real weather forecast
esp32s3_w5500_control / esp32s3_w5500_lowpower	The control registers / PHY power-down
esp32s3_multinic	Two interfaces at once: longest-prefix routing, per-socket pinning
esp32s3_modbus_master / esp32s3_modbus_slave	Modbus TCP, both ends
esp32s3_ftp / esp32s3_ftp_inet / esp32s3_ftp_server	FTP client (local, then a real internet server) / an anonymous server over the ext4 flash
esp32s3_dns_secure	One name, four DNS transports: UDP, TCP, DoT, DoH
esp32s3_tls_hello / esp32s3_tls_weather / esp32s3_tls_resume	Pure-Ada TLS 1.3: a handshake walkthrough / a live HTTPS fetch / resumption with a PSK ticket

Crypto and X.509 known-answer tests (no wiring, no network: the vectors are baked in, so each one is a self-contained PASS/FAIL on the board)

Example	What it is
esp32s3_p256_kat	Pure-Ada P-256 ECDSA verify + ECDH, against the standard vectors
esp32s3_rsa_kat / esp32s3_aes_gcm_kat	The RSA accelerator's modexp / AES-GCM authenticated encryption
esp32s3_sparknacl_kat	SPARKNaCl, the formally-verified crypto library, on the S3
esp32s3_x509_kat / esp32s3_x509_verify	DER certificate parsing / certificate signature verification
esp32s3_x509_chain / esp32s3_x509_policy	Chain validation / validity window + hostname (SAN) matching

Wi-Fi (link the fetched Apache-2.0 Espressif blobs — run tools/fetch-wifi-blobs.sh once, or set IDF_PATH; put your network in the gitignored src/wifi_credentials.ads)

Example	What it is
esp32s3_wifi_scan	Bring up the radio and list nearby access points
esp32s3_wifi_sniff	Promiscuous-mode 802.11 packet capture
esp32s3_wifi_dns	Associate + resolve a hostname (DNS_Client)
esp32s3_wifi_http	GET a URL over the pure-Ada software TCP stack
esp32s3_wifi_tls	Pure-Ada TLS 1.3 HTTPS end-to-end: assoc → DHCP → DNS → NTP → TLS handshake → chain-validate to ISRG Root X1 → live fetch
esp32s3_wifi_ecdsa	Pure-Ada P-256 / P-384 authenticating a real all-ECDSA chain: same pipeline, but the peer's chain is ECDSA to the root, so P256.Verify and P384.Verify do the work (reports which primitive verified which link)

Diagnostics

Example	What it is
esp32s3_intr_levels	Interrupt-vector regression test (L2/L3/L5 dispatch + context preservation)
esp32s3_shared_l2	Two drivers sharing one level-2 interrupt
esp32s3_delay_test	delay until accuracy: the SYSTIMER alarm, idle-then-wake
esp32s3_stack_usage	The runtime's own stack high-water mark, read back on the board
esp32s3_heaptest / esp32s3_stress	TLSF malloc/free under stress / the runtime stress suite
esp32s3_mac	The factory MAC addresses, read from eFuse

The peripheral HAL

libs/esp32s3_hal is a reusable GPR library project (with "esp32s3_hal.gpr"; — resolved by name via GPR_PROJECT_PATH, which export.sh sets; it is not an Alire crate, and only the runtime in crates/ is) of task-safe drivers built on an svd2ada register layer: GPIO, SPI, I2C, UART, GDMA, I2S, LEDC, RMT, PCNT, SDM, MCPWM, GP timers, ADC, capacitive touch, RTC + RTC-IO, LCD (i80), TWAI/CAN, hardware crypto (SHA/AES), RNG, and SD (SPI + native SDHOST). Each is a thin private register "Engine" hidden behind a task-safe gateway (protected object or a limited-controlled RAII handle), so concurrent access from multiple tasks is safe by construction. Most drivers ship with a self-test under examples/; see Testing status for what has actually been run on silicon.

Which drivers a build sees is decided by source directory, not by a list: light-tasking compiles src/ alone (the lock-free, finalization-free core), while embedded and full compile src/**. A driver that needs a controlled RAII handle, exceptions or the secondary stack lives in a subdirectory light-tasking never looks in, so adding a file defaults to safe — and ./x test lib builds the library on all three profiles to keep it that way.

The pure-Ada ext4 filesystem

libs/esp32s3_hal/src/ext4 is a from-scratch ext2/3/4 implementation in Ada (a reimplementation in the spirit of lwext4): read and write (create/write/truncate/mkdir/rmdir/unlink/rename/link), metadata checksums, and JBD2 journal replay + commit. It is developed against a rootless host test harness that checks every operation against mke2fs/debugfs/e2fsck (test/ext4_host, one of the suites ./x test host runs): 17 scenarios, each ending in a clean e2fsck -fn. It also runs on a card: esp32s3_ext4_sdmmc mounts a real mkfs.ext4 SD card over the native SDHOST, esp32s3_ext4_write puts the write battery through it as one journaled transaction, and the card passes e2fsck -f on a Linux host afterwards. On SPI NOR flash it runs over the wear-leveling FTL, including on-device Ext4.Mkfs. The one block adapter still unproven on a card is SD_SPI_Source (SD over SPI), which is what examples/esp32s3_ext4 uses.

The pure-Ada FAT16 filesystem

libs/esp32s3_hal/src/fat16 is the filesystem to reach for when a PC has to see the medium. A device that exposes its storage over USB mass storage appears as a removable drive; format it FAT and Windows, macOS and Linux all mount it with no driver and no ceremony. ext4 is the better filesystem, but only Linux mounts it.

ESP32S3.Fat16 reads — mount, list, open, read, seek — with long filenames, from either an MBR-partitioned disk (what Windows expects on a USB stick) or a bare boot sector at LBA 0. ESP32S3.Fat16.Mkfs formats blank media, choosing 4 KB clusters aligned to the NOR erase unit so the block layer's read-modify-write stays one erase per cluster written. FAT12 and FAT32 volumes are recognised and refused rather than misread. Both sit on ESP32S3.Block_Dev, so the same sources run over SPI NOR flash, an SD card, or a file-backed device in the test harness.

It is host-verified: the harness (test/fat16_host) makes three independent implementations agree about every volume — the Ada code, the host's own dosfstools (mkfs.fat writes volumes it must read, fsck.fat checks volumes it writes), and a FAT16 writer written from the specification rather than from the Ada source.

Programming another ESP32

libs/esp32s3_hal/src/esp_loader speaks the ESP32 serial ROM-bootloader protocol as the host, so a board can flash another ESP32 over a UART — the device-side twin of what esptool (and this SDK's own examples/common/bare/espflash) does from a PC. A production jig, a field programmer, or a board that reflashes its own daughterboard all need this, and none of them should have to run Python.

ESP32S3.Esp_Loader connects (reset into the download loader, then SYNC), raises the baud rate, and streams images: Begin_Image declares the length, Write takes whatever chunks the source produces, and full 1 KB blocks go out as they fill. Flashing a megabyte therefore costs a kilobyte of RAM, and a truncated source is an error rather than a corrupt target. ESP32S3.Esp_Loader.Serial_Link is the ready-made transport over a UART and two GPIOs. Only the ROM loader is spoken — no downloadable stub, so no compression; that costs transfer time and nothing else.

The whole family. Connect identifies the target, because the ROM protocol is not uniform and guessing wrong corrupts flash rather than failing cleanly: the original ESP32 ends every reply with four status bytes instead of two, the ESP32 and ESP8266 take a shorter FLASH_BEGIN payload, and the ESP8266 has no SPI_ATTACH at all plus a bug in how it sizes an erase. Identification uses GET_SECURITY_INFO where the chip supports it (ESP32-S3 and later) and the magic register otherwise (ESP8266, ESP32, ESP32-S2) — ESP8266, ESP32, S2, S3, C2, C3, C5, C6, C61, H2, H21, H4, P4, S31 and E22. A chip newer than the table still connects, as Unknown, and is driven with the modern defaults.

Pass-through too. ESP32S3.Esp_Loader.Auto_Reset is the auto-reset circuit every ESP development board has, in software: when a board sits between a PC and a target as a USB-serial bridge, esptool on the PC expects to reach the target's ROM loader by wiggling DTR and RTS, and this makes that work. It reproduces the real circuit's cross-coupling — so a terminal emulator asserting both lines on open does not reset the target — and emulates its capacitor, so esptool's ClassicReset (which moves the lines one at a time) works regardless of what the target board has on its EN pin.

It is host-verified only: test/esp_loader_host drives it against a simulated ROM that validates every frame it is sent, impersonating each chip family in turn — and deliberately breaks the per-chip handling three ways to prove those checks bite. The real ROM's timing and quirks still want a target board on the end of a real UART.

Testing status

Important: the table below reflects what was exercised during development; nothing here has been re-verified as it ships in this distribution. Treat every driver as needing verification on your own board before you rely on it.

Drivers that have a hardware self-test (loopback or self-test run on an ESP32-S3 during development — re-verify on your hardware):

GPIO (+ level-3 interrupts), RNG, SPI, I2C, UART, GDMA, I2S, LEDC, RMT, PCNT, SDM, MCPWM, GP Timer (TIMG), ADC, capacitive Touch, RTC, RTC-IO, LCD (i80), TWAI/CAN, SHA, AES.

External devices with an on-board example but no automatic self-test — each needs the part wired up, and the example prints what it saw:

W5500 Ethernet, Wi-Fi (radio + software TCP/IP), SDMMC (a real ext4 card, read and written), W25Q SPI NOR, ST7789 and i80 panels, GT911 touch, ES8311 codec, TX1812 LED string, TLV2556 ADC, SHT41, QMI8658C, PCF85063A, TCA9555, CH422G, HC595, M24C64 / 24Cxx EEPROM, FRAM, NMEA GPS.

Protocol libraries that ride on the network stack — DNS, NTP, FTP (client and server), Modbus (master and slave), X.509, TLS 1.3 — are exercised by host suites against real servers (./x test host), and each has an on-board example; the host suite is the automatic part, the board example is not.

Drivers and components that are not hardware-verified and need testing:

Component	State	What's needed
SD_SPI (SD card over SPI)	compiles; no-card smoke test only	test against a real card
Temperature sensor	compiles	run on hardware
FAT16 filesystem	host-verified vs dosfstools only	validate on-device over SPI NOR
ESP serial bootloader client	host-verified vs a simulated ROM only	validate against a real target over UART

What CI checks on every push

./x test — the same command you can run locally — and nothing in it needs a board: every library on every runtime profile it supports (warnings are failures), a build of all 97 examples, and the host suites. Hardware validation stays on the bench; CI's job is that the tree still builds and the portable logic still passes.

Proof and static analysis

Two board-free gates sit alongside the test suites, and neither is a claim that the code is clean: each one is a tripwire that only reports something new.

SPARK proof. book/prove/prove.sh runs GNATprove over the pure, bounded units: the parsers, serializers and checksums that handle untrusted or integrity-critical data. 32 units, 1,939 obligations, zero unproved — 1,076 of them run-time checks (no overflow, no buffer overrun, every loop terminates), and 273 functional contracts that say what the code computes. The untrusted-input parsers are the point: X509, NMEA, DNS_Client.Parse, Chain_Verify, P256.Verify and the Modbus slave and master provably cannot overrun, overflow or loop forever on any malformed input. Nine units go past that floor to gold or platinum, where the contract pins the answer rather than just the safety. Proving found five real defects and three specification gaps that silver could not see — an X509 hostname match that could index out of range, a Chain_Verify null dereference, an NTP_Client conversion that admitted February 31st. The unit table, the levels and the bug list are in book/prove/README.md; the book's Formal Proof with SPARK and Static Analysis chapters cover the method.

Static analysis. ./x analyze runs adalang_analyzer (Maurizio Martignano's Libadalang-based analyser, an Alire crate) over each library and filters out everything already fingerprinted in tools/analyzer-baselines/, so it prints only what a change introduced. ./x analyze --style is the second rule set (complexity, duplication, constructs that obscure intent) against its own baseline, and ./x analyze --do178c writes per-objective DO-178C evidence reports — a report for a certification process to consume, not a gate. The analyzer is deliberately not part of ./x test: it is not in the toolchain this project pins, so a plain clone would fail a check it cannot run.

Footprint. ./x stack <example> reports per-frame and worst-case call-chain stack use (--run adds the measured high-water mark over serial), and ./x mem <example> reports section sizes against the linker's bounds.

ACATS conformance

The runtime is exercised against the ACATS 4.2 suite on real hardware, one test per flashed image, with the grade captured per test over the serial console. Last run 2026-09-05 against a96a9a7:

Profile	applicable	passed	na	exception	hung	nobuild
light-tasking (Jorvik)	1132	674	3	93	0	361
embedded (ZCX)	1257	884	3	2	0	368
full (complete GNARL)	1559	908	5	2	1	643

Reconciled across all three profiles (richest = full as the reference, with a host-GNAT cross-check on every genuine signal): 762 conformant, 151 profile-limited, 643 absent-unit, 55 not-run, 2 not-ours, 1 known-limitation, and zero port-specific defects.

• exception on light-tasking is overwhelmingly deliberately-raised exceptions that cannot propagate under No_Exception_Propagation — they pass on the richer profiles. nobuild is the absent-unit boundary (Ada.Calendar, file I/O, Ada.Finalization).
• The one hung is CXE4006, an Annex E remote-call server: a single-node target has no client partition, so it waits forever. Inapplicable, not a defect.
• The two not-ours (C3A1005, CC51011) fail identically on stock host x86 GNAT, so they are target-independent rather than this port's. Both are new tests in ACATS Modification List 4.2A (June 2024); the RM analysis suggests the tests themselves are at fault. See the full report for the rules and the reasoning.

Full report: Ada_esp32s3_acats/ACATS_RESULTS.md — per-profile tallies, terminology, the reconciliation, and every bug the sweeps found and fixed. The suite and its harness are not shipped here; they live in that repository, which pulls this one in as a submodule.

Tooling & debugging

• ./x — the in-repo dispatcher (build/flash/monitor/new/debug). ./x list shows every example and its profile.
• ./x test — everything checkable without a board, in one command: the host suites, every library on every profile it supports (warnings fail the build), and a build of all 97 examples. This is exactly what CI runs. Narrow it with ./x test host, ./x test lib, ./x test examples.
• ./x analyze — static analysis against a per-library baseline, so only new findings are reported (--style for the readability set, --do178c for evidence reports). See Proof and static analysis.
• ./x stack / ./x mem — worst-case stack per call chain (--run measures the real high-water mark) and the image's section sizes against the linker map.
• esp32-ada — after source export.sh, scaffold and build projects in any empty folder, no runtime source copied.
• VS Code — first-class target: build tasks plus on-chip GDB debugging over the built-in USB-Serial-JTAG (pinned OpenOCD + Xtensa GDB). Rests at Ada Main.
• Flashing uses our own Ada esp_flash host tool (no esptool needed; ESP_USE_ESPTOOL=1 is an optional fallback).

Details and editor setup: TOOLING.md.

Repository layout

crates/
  esp32s3_rts/      the GNAT runtime crate (3 profiles) + gen_runtime.sh + full_overlay/
  bb-runtimes/      AdaCore bb-runtimes fork with the esp32s3 board (submodule)
  xtensa-dynconfig/ the Xtensa core-config plugin the toolchain needs
libs/
  esp32s3_hal/      the reusable peripheral HAL + the pure-Ada ext4/FAT16 filesystems
    src/            lock-free / pure-logic core -- available on EVERY profile
    src/peripherals/  on-chip drivers with an RAII Session/Channel handle
    src/devices/      off-chip parts reached over those (sensors, panels, flash)
    src/net/          Net_Devices + W5500, the GNAT.Sockets facade, DNS/NTP/FTP/Modbus
    src/ext4/ fat16/ eeprom/ fram/ esp_loader/ text_io/
    svd/            the svd2ada register layer (generated; see regenerate.sh)
  tls/              pure-Ada TLS 1.3 + X.509 path validation
  esp32s3_wifi/     the Wi-Fi driver (Ada, over Espressif's fetched PHY/MAC blobs)
  esp32s3_simd/     vendored Xtensa PIE SIMD kernels
examples/           the flashable examples (each owns its board.ads)
  common/bare/      the shared FreeRTOS-free boot (bootloader, start.S, vectors, glue)
book/               the long-form guide (LaTeX sources + main.pdf)
  prove/            the SPARK proof surface (prove.sh + what is proved, and to what level)
docs/               the static getting-started site (adaformicrocontrollers.com)
tools/              fetch-wifi-blobs.sh, the analyzer baselines, host helpers
ide/                the VS Code and Vim integrations
x, export.sh        the ./x dispatcher and the esp32-ada launcher
QUICKSTART.md, TOOLING.md

Prerequisites

• Alire (alr) with the gnat_xtensa_esp32_elf and gnat_native toolchains + gprbuild (Alire fetches them on first build).
• A host C compiler (to build the xtensa-dynconfig plugin once).
• An ESP32-S3 board on USB. Console is the built-in USB-Serial-JTAG (/dev/ttyACM*) or an external UART bridge (CH343/FTDI).

The bare boot runs with memory protection (W^X) off, which the Ada task-body trampolines require; there is no sdkconfig/idf.py involved.

Status

The runtime and all three profiles build and run on hardware (the examples flash and boot). The HAL drivers and the filesystem have varying levels of verification — see Testing status; several need testing on hardware and nothing has been re-verified as it ships here. The full profile is functionally complete for the common cases; its remaining edges (an RM-permitted abort case, a couple of toolchain-bound constructs, and post-2099 Ada.Calendar) are catalogued in the book's Full-Profile Limitations chapter. The project name dropped the original "Jorvik" branding; the genuine Ada Jorvik profile support remains.

License

Apache-2.0 WITH LLVM-exception (see LICENSE and NOTICE). The runtime builds on AdaCore's GPL-3-with-runtime-exception bb-runtimes; the GNAT Runtime Library Exception applies to code linked against the runtime.