Hume
(Higher-order Unified Meta-Environment) is a strongly typed, mostly-functional programming language with an integrated tool set for developing, proving and assessing concurrent, safety-critical systems. Hume aims to extend the frontiers of language design for resource-limited systems, including real-time embedded and safety-critical systems, by introducing new levels of abstraction and provability. Citation from its home page (see below).