Пятнадцать байтов на стек от конца

Оказывается, язык Ада не умер, а плавно превратился в SPARK. 

SPARK 2014 Reference Manual: http://docs.adacore.com/spark2014-docs/html/lrm/

Книга, объясняющая методологию использования языка SPARK для разработки систем высокой надёжности: https://www.adacore.com/uploads/books/pdf/ePDF-ImplementationGuidanceSPARK.pdf

Исходники микроядра Muen, написанного на SPARK: https://muen.codelabs.ch/