ccg GNAT Spark ada AdaCore SPARK и Ada на любой платформе. Похоже, грядёт замена AdaMagic, которая будет поддерживать последние стандарты и будет более открытой.

У тормозов прогресса будет меньше нелепых оправданий

Coq Spark ada Вынос лемм в отдельные пакеты

конкурс Spark ARM ada embedded Началось соревнование «Make with Ada» для разработчиков встраиваемых систем
AdaCore организует новый конкурс для разработчиков. Как и в прошлые разы, на подготовку даётся существенно больше времени, чем в олимпиадах по иноформатике. Это как раз подходит тем, кому не нравятся соревнования по быстрому написанию страшного кода, который потом только выбросить.

Сегодня на повестке дня — разработка для ARM на голом железе и технологии верификации. Общий призовой фонд — более 8000€.
makewithada.org

Как бы отвечая на напрашивающийся вопрос, — да, я уже посмотрел на логотип через анаглиф очки.

DNS Spark ada ironsides.martincarlisle.com
Адский DNS сервер

IRONSIDES is an authoritative/recursive DNS server pair that is provably invulnerable to many of the problems that plague other servers. It achieves this property through the use of formal methods in its design, in particular the language Ada and the SPARK formal methods tool set. Code validated in this way is provably exception-free, contains no data flow errors, and terminates only in the ways that its programmers explicitly say that it can. These are very desirable properties from a computer security perspective.