Ada and SPARK on Cortex-M - tutorial with Arduino and Nucleo examples