SPARK is defacto, safe language for embedded. Smallest I heard it used on was 8-bit AVR: https://en.m.wikipedia.org/wiki/SPARK_(programming_language) https://e

SPARK is defacto, safe language for embedded. Smallest I heard it used on was 8-bit AVR: https://en.m.wikipedia.org/wiki/SPARK_(programming_language) https://en.m.wikipedia.org/wiki/SPARK_(programming_language) Ivory might git your requirements: http://ivorylang.org/ivory-introduction.html http://ivorylang.org/ivory-introduction.html Tower is their other one: https://github.com/GaloisInc/tower/blob/master/README.md https://github.com/GaloisInc/tower/blob/master/README.md ATS is used here on an 8-bitter: https://github.com/fpiot/arduino-ats/blob/master/README.md https://github.com/fpiot/arduino-ats/blob/master/README.md