In 2014, AdaCore has released two new components in the GNAT GPL Edition: GNAT GPL for ARM Bare Board and SPARK 2014. I present the content of GNAT GPL for ARM, its Ravenscar runtime, how to build and deploy an embedded application in Ada and how it was used to teach Ada.

Two different demos will be presented: a Tetris game and a train signalling system. Both are fully written in Ada, with some parts written and proven with SPARK 2014.